Commit 2019-04-09 04:27 eb024dc8
View on Github →feat(order/lexicographic): lexicographic pre/partial/linear orders (#820)
- remove prod.(*)order instances
- feat(order/lexicographic): lexicographic pre/partial/linear orders
- add lex_decidable_linear_order
- identical constructions for dependent pairs
- cleaning up
- Update lexicographic.lean
forgotten
instance - restore product instances, and add lex type synonym for lexicographic instances
- proofs in progress
-
- define lt
- prove lt_iff_le_not_le
- refactoring