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 α
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    unsafe def Lean.Meta.evalExpr' (α : Type) (typeName : Lean.Name) (value : Lean.Expr) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) :
    Lean.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 : Lean.Expr) (safety : Lean.DefinitionSafety := Lean.DefinitionSafety.safe) :
      Lean.MetaM α
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For