def Lean.Elab.Command.elabPrint : Lean.Elab.Command.CommandElab

Equations

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

structure Lean.Elab.Command.CollectAxioms.State : Type

• visited : Lean.NameSet
• axioms : Array Lake.Name

@[inline, reducible]

abbrev Lean.Elab.Command.CollectAxioms.M (α : Type) : Type

Equations

• Lean.Elab.Command.CollectAxioms.M = ReaderT Lean.Environment (StateM Lean.Elab.Command.CollectAxioms.State)

partial def Lean.Elab.Command.CollectAxioms.collect (c : Lake.Name) : Lean.Elab.Command.CollectAxioms.M Unit

def Lean.Elab.Command.elabPrintAxioms : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabPrintEqns : Lean.Elab.Command.CommandElab

Equations

• Lean.Elab.Command.elabPrintEqns stx = let id := stx[2]; do let cs ← Lean.Elab.resolveGlobalConstWithInfos id List.forM cs Lean.Elab.Command.printEqnsOf