Documentation

Lean.Meta.Check

source
def Lean.Meta.throwLetTypeMismatchMessage {α : Type} (fvarId : Lean.FVarId) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.addPPExplicitToExposeDiff (a : Lean.Expr) (b : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Meta.addPPExplicitToExposeDiff.visit (a : Lean.Expr) (b : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)
source
partial def Lean.Meta.addPPExplicitToExposeDiff.hasExplicitDiff? (xs : Array Lean.Expr) (as : Array Lean.Expr) (bs : Array Lean.Expr) :
Lean.MetaM (Option (Array Lean.Expr × Array Lean.Expr))
source
def Lean.Meta.mkHasTypeButIsExpectedMsg (givenType : Lean.Expr) (expectedType : Lean.Expr) :
Lean.MetaM Lean.MessageData
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.throwAppTypeMismatch {α : Type} (f : Lean.Expr) (a : Lean.Expr) :
Lean.MetaM α
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.checkApp (f : Lean.Expr) (a : Lean.Expr) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.check (e : Lean.Expr) :
Lean.MetaM Unit
Equations
source
def Lean.Meta.isTypeCorrect (e : Lean.Expr) :
Lean.MetaM Bool
Equations
  • One or more equations did not get rendered due to their size.