Commit 2022-01-12 22:49 e6fab1dc

refactor(order/directed): Make is_directed a Prop mixin (#11238) This turns directed_order into a Prop-valued mixin is_directed. The design follows the unbundled relation classes found in core Lean. The current design created obscure problems when showing that a semilattice_sup is directed and we couldn't even state that semilattice_inf is codirected. Further, it was kind of already used as a mixin, because there was no point inserting it in the hierarchy.