Documentation

Lean.Elab.BuiltinEvalCommand

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.
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.
source
def Lean.Elab.Command.elabEvalBang :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabRunCmd :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabRunElab :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Command.elabRunMeta :
CommandElab
Equations
  • One or more equations did not get rendered due to their size.