#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.

inductive Lean.Elab.Tactic.GuardMsgs.SpecResult : Type

The decision made by a specification for a message.

• check: Lean.Elab.Tactic.GuardMsgs.SpecResult

  Capture the message and check it matches the docstring.

• drop: Lean.Elab.Tactic.GuardMsgs.SpecResult

  Drop the message and delete it.

• passthrough: Lean.Elab.Tactic.GuardMsgs.SpecResult

  Do not capture the message.

def Lean.Elab.Tactic.GuardMsgs.parseGuardMsgsSpec (spec? : Option (Lean.TSyntax `Lean.guardMsgsSpec)) : Lean.Elab.Command.CommandElabM (Lean.Message → Lean.Elab.Tactic.GuardMsgs.SpecResult)

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.

structure Lean.Elab.Tactic.GuardMsgs.GuardMsgFailure : Type

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

• res : String

  The result of the nested command

instance Lean.Elab.Tactic.GuardMsgs.instTypeNameGuardMsgFailure : TypeName Lean.Elab.Tactic.GuardMsgs.GuardMsgFailure

Equations

• Lean.Elab.Tactic.GuardMsgs.instTypeNameGuardMsgFailure = Lean.Elab.Tactic.GuardMsgs.inst✝

def Lean.Elab.Tactic.GuardMsgs.elabGuardMsgs : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Tactic.GuardMsgs.guardMsgsCodeAction : Lean.CodeAction.CommandCodeAction

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

Equations

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