From 8032d2eefd9de487f4a7adc642f4ede373cdfb5e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Dec 2017 16:48:31 -0800 Subject: [PATCH] feat(library/init/algebra/order): add instance --- library/init/algebra/order.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/library/init/algebra/order.lean b/library/init/algebra/order.lean index c93e0541a6..ab424df157 100644 --- a/library/init/algebra/order.lean +++ b/library/init/algebra/order.lean @@ -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 (<) }