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 : SpecResult

    Capture the message and check it matches the docstring.

  • drop : SpecResult

    Drop the message and delete it.

  • pass : SpecResult

    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
        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
            • One or more equations did not get rendered due to their size.
            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 protectes 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