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.

Instances For

    The method to use when normalizing whitespace, after trimming.

    Instances For

      Method to use when combining multiple messages.

      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

              Applies a message ordering mode.

              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