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

Equations

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

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.Command.liftCoreM (Lean.Elab.realizeGlobalConstWithInfos id) cs.forM Lean.Elab.Command.printEqnsOf