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.