Documentation

Mathlib.Tactic.Relation.Symm

relSidesIfSymm? #

This may now be orphaned code which can be removed.

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.
Instances For