max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/algebra/order): add instance

Browse source
This commit is contained in:
Leonardo de Moura 2017-12-02 16:48:31 -08:00
parent 450ca5834c
commit 8032d2eefd
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/algebra/order.lean
View file

@ -234,3 +234,11 @@ instance [decidable_linear_order α] : is_total_preorder α (≤) :=
/- TODO(Leo): decide whether we should keep this instance or not -/
instance is_strict_weak_order_of_decidable_linear_order [decidable_linear_order α] : is_strict_weak_order α (<) :=
is_strict_weak_order_of_is_total_preorder lt_iff_not_ge
/- TODO(Leo): decide whether we should keep this instance or not -/
instance is_strict_total_order_of_decidable_linear_order [decidable_linear_order α] : is_strict_total_order α (<) :=
{ trichotomous := lt_trichotomy,
/- TODO: use ..is_strict_weak_order_of_decidable_linear_order -/
trans := λ _ _ _, trans_of (<),
irrefl := irrefl_of (<),
incomp_trans := λ _ _ _, incomp_trans_of (<) }