@[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 α)

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 : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.matchFalse e = Lean.Meta.testHelper e fun e => pure (Lean.Expr.isConstOf e `False)

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.

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)

Equations

• Lean.Meta.matchConstructorApp? e = do let env ← Lean.getEnv Lean.Meta.matchHelper? e fun e => pure (Lean.Expr.isConstructorApp? env e)