@[inline]
Instances For
@[inline]
def
Lean.Meta.matchHelper?
{α : Type}
(e : Lean.Expr)
(p? : Lean.Expr → Lean.MetaM (Option α))
:
Lean.MetaM (Option α)
Instances For
Matches e with lhs = (rhs : α) and returns (α, lhs, rhs).
Instances For
Return some (α, lhs, rhs) if e is of the form @Eq α lhs rhs or @HEq α lhs α rhs