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 = do let cs ← Lean.Elab.Command.liftCoreM (Lean.Elab.realizeGlobalConstWithInfos stx[2]) cs.forM Lean.Elab.Command.printEqnsOf