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