Documentation

Lean.Meta.MatchUtil

source
@[inline]
def Lean.Meta.testHelper (e : Lean.Expr) (p : Lean.Expr → Lean.MetaM Bool) :
Lean.MetaM Bool
Equations
source
@[inline]
def Lean.Meta.matchHelper? {α : Type} (e : Lean.Expr) (p? : Lean.Expr → Lean.MetaM (Option α)) :
Lean.MetaM (Option α)
Equations
source
def Lean.Meta.matchEq? (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
Equations
source
def Lean.Meta.matchHEq? (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))
Equations
source
def Lean.Meta.matchEqHEq? (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

Return some (α, lhs, rhs) if e is of the form @Eq α lhs rhs or @HEq α lhs α rhs

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.matchFalse (e : Lean.Expr) :
Lean.MetaM Bool
Equations
source
def Lean.Meta.matchNot? (e : Lean.Expr) :
Lean.MetaM (Option Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.matchNe? (e : Lean.Expr) :
Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.matchConstructorApp? (e : Lean.Expr) :
Lean.MetaM (Option Lean.ConstructorVal)
Equations