Documentation

Lean.Elab.GuardMsgs

#guard_msgs command for testing commands

This module defines a command to test that another command produces the expected messages. See the docstring on the #guard_msgs command.

The decision made by a specification for a message.

  • check : FilterSpec

    Capture the message and check it matches the docstring.

  • drop : FilterSpec

    Drop the message and delete it.

  • pass : FilterSpec

    Do not capture the message.

Instances For

    The method to use when normalizing whitespace, after trimming.

    Instances For

      Method to use when combining multiple messages.

      Instances For

        The specification options for #guard_msgs. The default field values provide the default behavior of #guard_msgs.

        Instances For
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Parses a GuardMsgsSpec.

              • No specification: check everything.
              • With a specification: interpret the spec, and if nothing applies pass it through.
              Equations
              Instances For

                An info tree node corresponding to a failed #guard_msgs invocation, used for code action support.

                • res : String

                  The result of the nested command

                Instances For

                  Makes trailing whitespace visible and protects them against trimming by the editor, by appending the symbol ⏎ to such a line (and also to any line that ends with such a symbol, to avoid ambiguities in the case the message already had that symbol).

                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      A code action which will update the doc comment on a #guard_msgs invocation.

                      Equations
                      Instances For