Add instances of total orders

agda · Nov 15, 2024 · 70a6c7a · 70a6c7a
1 parent 3b82fcb
commit 70a6c7a
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Class/HasOrder/Instance.agda b/Class/HasOrder/Instance.agda
@@ -20,16 +20,25 @@ instance
   ℕ-hasPartialOrder = HasPartialOrder ∋ record
     { ≤-antisym = Nat.≤-antisym }
   ℕ-hasDecPartialOrder = HasDecPartialOrder {A = ℕ} ∋ record {}
+  ℕ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Nat.≤-total }
+  ℕ-hasDecTotalOrder = HasDecTotalOrder {A = ℕ} ∋ record {}
 
   import Data.Integer.Properties as Int hiding (_≟_)
   ℤ-hasPreorder = HasPreorder ∋ record {Int; ≤⇔<∨≈ = let open Int in mk⇔
     (λ a≤b → case _ ≟ _ of λ where (yes p) → inj₂ p ; (no ¬p) → inj₁ (≤∧≢⇒< a≤b ¬p))
     [ <⇒≤ , ≤-reflexive ] }
   ℤ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Int.≤-antisym }
   ℤ-hasDecPartialOrder = HasDecPartialOrder {A = ℤ} ∋ record {}
+  ℤ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Int.≤-total }
+  ℤ-hasDecTotalOrder = HasDecTotalOrder {A = ℤ} ∋ record {}
 
   import Data.Rational.Properties as Rat hiding (_≟_)
 
   ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
   ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
   ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
+  ℚ-hasTotalOrder = HasTotalOrder ∋ record
+    { ≤-total = Rat.≤-total }
+  ℚ-hasDecTotalOrder = HasDecTotalOrder {A = ℚ} ∋ record {}