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

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

Instances For

source
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)

Instances For

source
def Lean.Elab.Command.elabPrintAxioms :
CommandElab
Equations

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

Instances For

source
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✝

Instances For