def Lean.Elab.Command.elabPrint : CommandElab

Equations

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

def Lean.Elab.Command.elabPrintAxioms : CommandElab

Equations

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

def Lean.Elab.Command.elabPrintEqns : 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✝