# Documentation

Lean.Meta.MatchUtil

@[inline]
def Lean.Meta.testHelper (e : Lean.Expr) (p : ) :
Equations
• = do let __do_lift ← p e if __do_lift = true then else do let __do_lift ← p __do_lift
@[inline]
def Lean.Meta.matchHelper? {α : Type} (e : Lean.Expr) (p? : ) :
Equations
• = do let __do_lift ← p? e match __do_lift with | none => do let __do_lift ← p? __do_lift | s => pure s

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

Equations

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.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations