@[inline]

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

Equations

• Lean.Meta.testHelper e p = do let __do_lift ← p e if __do_lift = true then pure true else do let __do_lift ← Lean.Meta.whnf e p __do_lift

@[inline]

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

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

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

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

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.

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

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

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.

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