HepLean 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 α
Instances For
    source
    unsafe def Lean.Meta.evalExpr' (α : Type) (typeName : Lake.Name) (value : Lean.Expr) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) :
    Lean.MetaM α
    Instances For
      source
      unsafe def Lean.Meta.evalExpr (α : Type) (expectedType : Lean.Expr) (value : Lean.Expr) (safety : optParam Lean.DefinitionSafety Lean.DefinitionSafety.safe) :
      Lean.MetaM α
      Instances For