Documentation

Lean.Meta.Eval

source
unsafe def Lean.Meta.evalExprCore (α : Type) (value : Lean.Expr) (checkType : Lean.Expr → Lean.MetaM Unit) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Meta.evalExpr' (α : Type) (typeName : Lean.Name) (value : Lean.Expr) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.
source
unsafe def Lean.Meta.evalExpr (α : Type) (expectedType : Lean.Expr) (value : Lean.Expr) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.