relSidesIfSymm?

def Lean.Expr.relSidesIfSymm? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Name × Lean.Expr × Lean.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.