Documentation
Lean
.
Elab
.
Eval
Search
return to top
source
Imports
Lean.Elab.SyntheticMVars
Lean.Meta.Eval
Imported by
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.
Instances For