Documentation
Lean
.
Elab
.
Eval
Search
Google site search
return to top
source
Imports
Init
Lean.Elab.SyntheticMVars
Lean.Meta.Eval
Imported by
Lean
.
Elab
.
Term
.
evalTerm
source
unsafe def
Lean
.
Elab
.
Term
.
evalTerm
(α :
Type
)
(type :
Lean.Expr
)
(value :
Lean.Syntax
)
(safety :
optParam
Lean.DefinitionSafety
Lean.DefinitionSafety.safe
)
:
Lean.Elab.TermElabM
α
Equations
One or more equations did not get rendered due to their size.
Instances For