Documentation

Lean.Elab.Print

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 Lean.Name

@[inline]

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 : Lean.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.