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