@[inline]

def Lean.Meta.testHelper (e : Expr) (p : Expr → MetaM Bool) : 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 : Expr) (p? : Expr → MetaM (Option α)) : MetaM (Option α)

Equations

• Lean.Meta.matchHelper? e p? = do let __do_lift ← p? e match __do_lift with | none => do let __do_lift ← Lean.Meta.whnf e p? __do_lift | s => pure s

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

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

Equations

• Lean.Meta.matchEq? e = Lean.Meta.matchHelper? e fun (e : Lean.Expr) => pure e.eq?

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

Equations

• Lean.Meta.matchHEq? e = Lean.Meta.matchHelper? e fun (e : Lean.Expr) => pure e.heq?

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.matchFalse e = Lean.Meta.testHelper e fun (e : Lean.Expr) => pure e.isFalse

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.matchConstructorApp? e = Lean.Meta.matchHelper? e Lean.Meta.isConstructorApp?