HepLean Documentation

Lean.Meta.Eval

source
unsafe def Lean.Meta.evalExprCore (α : Type) (value : Lean.Expr) (checkType : Lean.Expr → Lean.MetaM Unit) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) :
Lean.MetaM α
Instances For
    source
    unsafe def Lean.Meta.evalExpr' (α : Type) (typeName : Lean.Name) (value : Lean.Expr) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) :
    Lean.MetaM α
    Instances For
      source
      unsafe def Lean.Meta.evalExpr (α : Type) (expectedType value : Lean.Expr) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) :
      Lean.MetaM α
      Instances For