Documentation

Lean.Elab.Print

source
def Lean.Elab.Command.elabPrint :
Lean.Elab.Command.CommandElab
Instances For
    source
    structure Lean.Elab.Command.CollectAxioms.State :
    Type
    Instances For
      source
      @[inline, reducible]
      abbrev Lean.Elab.Command.CollectAxioms.M (α : Type) :
      Type
      Instances For
        source
        partial def Lean.Elab.Command.CollectAxioms.collect (c : Lake.Name) :
        Lean.Elab.Command.CollectAxioms.M Unit
        source
        def Lean.Elab.Command.elabPrintAxioms :
        Lean.Elab.Command.CommandElab
        Instances For