@[inline]

def Lean.Meta.testHelper (e : Expr) (p : Expr → MetaM Bool) : MetaM Bool

@[inline]

def Lean.Meta.matchHelper? {α : Type} (e : Expr) (p? : Expr → MetaM (Option α)) : MetaM (Option α)

def Lean.Meta.matchEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr))

Matches e with lhs = (rhs : α) and returns (α, lhs, rhs).

def Lean.Meta.matchHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr × Expr))

def Lean.Meta.matchEqHEq? (e : Expr) : MetaM (Option (Expr × Expr × Expr))

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

def Lean.Meta.matchEqHEqLHS? (e : Expr) : MetaM (Option (Expr × Expr))

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

def Lean.Meta.matchFalse (e : Expr) : MetaM Bool

def Lean.Meta.matchNot? (e : Expr) : MetaM (Option Expr)

def Lean.Meta.matchNe? (e : Expr) : MetaM (Option (Expr × Expr × Expr))

def Lean.Meta.matchConstructorApp? (e : Expr) : MetaM (Option ConstructorVal)