def
Lean.Elab.ContextInfo.runMetaMInCommandElabM
{α : Type}
(info : ContextInfo)
(lctx : LocalContext)
(x : MetaM α)
:
A copy of ContextInfo.runMetaM that keeps the messages and passes in the same filename.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Command.Linter.runTermLinter
{σ : Type}
[Inhabited σ]
(opt : Lean.Option Bool)
(lint : Term → Expr → StateT σ MetaM Unit)
:
A linter that applies to terms.
The lint argument receives both the original syntax and elaborated expression,
provided the option is enabled.
Note that the linter lives in StateT σ, so that it can build up state inherited from parent trees.
This doesn't return a Linter, as then the caller would have to remember to pass the name.
Equations
- One or more equations did not get rendered due to their size.