← Mathematical handbook

def Lean.Elab.Command.elabPrint : CommandElab

Equations

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

def Lean.Elab.Command.elabPrintSig : CommandElab

Equations

• Lean.Elab.Command.elabPrintSig stx = Lean.withRef stx[0] (have id := stx[2]; Lean.Elab.Command.printIdSig✝ id)

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✝