Documentation
Lean
.
Elab
.
Eval
Search
return to top
source
Imports
Lean.Elab.SyntheticMVars
Lean.Meta.Eval
Imported by
Lean.Elab.Tactic.BuiltinTactic
Lake.Util.Version
Lean.Elab.BuiltinCommand
Lean.Elab
Mathlib.Tactic.SuccessIfFailWithMsg
Lean.Elab.BuiltinTerm
Lean.Widget.UserWidget
Mathlib.Tactic.ApplyWith
Lean.Elab.BuiltinNotation
Lake.DSL.Meta
Lean
.
Elab
.
Term
.
evalTerm
source
unsafe def
Lean
.
Elab
.
Term
.
evalTerm
(α :
Type
)
(type :
Expr
)
(value :
Syntax
)
(safety :
DefinitionSafety
:=
DefinitionSafety.safe
)
:
TermElabM
α
Equations
One or more equations did not get rendered due to their size.