relSidesIfSymm?

def Lean.Expr.relSidesIfSymm? (e : Expr) : MetaM (Option (Name × Expr × Expr))

If e is the form @R .. x y, where R is a symmetric relation, return some (R, x, y). As a special case, if e is @HEq α a β b, return some (`HEq, a, b).

Equations

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