# Implementation of `#eval` command #

source
opaque Lean.Elab.Command.eval.pp :
Lean.Option Bool
source
opaque Lean.Elab.Command.eval.type :
Lean.Option Bool
source
opaque Lean.Elab.Command.eval.derive.repr :
Lean.Option Bool
source
unsafe def Lean.Elab.Command.elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) :
CommandElabM Unit
Equations

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

Instances For

source
@[implemented_by Lean.Elab.Command.elabEvalCoreUnsafe]
opaque Lean.Elab.Command.elabEvalCore (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) :
CommandElabM Unit
source
def Lean.Elab.Command.elabEval :
CommandElab
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For