mathlib
7f60a62d - chore(order/basic): move unbundled order classes to `rel_classes (#3066)

Commit
5 years ago
chore(order/basic): move unbundled order classes to `rel_classes (#3066) Reason: these classes are rarely used in `mathlib`, we don't need to mix them with classes extending `has_le`.
Author
Parents
Loading