Documentation

Lean.Meta.Eval

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