Documentation
Lean
.
Elab
.
Eval
Search
Google site search
return to top
source
Imports
Lean.Elab.SyntheticMVars
Lean.Meta.Eval
Imported by
Lean.Widget.UserWidget
Lean.Elab.BuiltinNotation
Lake.Util.Version
Lake.DSL.Meta
Lean.Elab.BuiltinTerm
Lean.Elab.BuiltinCommand
Lean.Elab.Tactic.BuiltinTactic
Lean.Elab
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
α