From 930c2a817fadc6481a40a370aba6dc087b0df469 Mon Sep 17 00:00:00 2001
From: whatisRT <andre.knispel@iohk.io>
Date: Thu, 7 Dec 2023 11:12:49 +0100
Subject: [PATCH] =?UTF-8?q?Add=20`=5F=E2=89=A5=5F`=20and=20`=5F>=5F`=20to?=
 =?UTF-8?q?=20`HasPreorder`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Interface/HasOrder.agda          |  5 ++++-
 src/Interface/HasOrder/Instance.agda | 10 ++++++++++
 src/Prelude.agda                     |  2 +-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/Interface/HasOrder.agda b/src/Interface/HasOrder.agda
index 032cc8750..ec7b56257 100644
--- a/src/Interface/HasOrder.agda
+++ b/src/Interface/HasOrder.agda
@@ -11,13 +11,16 @@ module _ {a} {A : Set a} where
   module _ {_≈_ : Rel A a} where
 
     record HasPreorder : Set (sucˡ a) where
-      infix 4 _≤_ _<_
+      infix 4 _≤_ _<_ _≥_ _>_
       field
         _≤_ _<_       : Rel A a
         ≤-isPreorder  : IsPreorder _≈_ _≤_
         <-irrefl      : Irreflexive _≈_ _<_
         ≤⇔<∨≈         : ∀ {x y} → x ≤ y ⇔ (x < y ⊎ x ≈ y)
 
+      _≥_ = flip _≤_
+      _>_ = flip _<_
+
       open IsPreorder ≤-isPreorder public
         using ()
         renaming (isEquivalence to ≈-isEquivalence; refl to ≤-refl; trans to ≤-trans)
diff --git a/src/Interface/HasOrder/Instance.agda b/src/Interface/HasOrder/Instance.agda
index 6b0b4a59f..71fde50e9 100644
--- a/src/Interface/HasOrder/Instance.agda
+++ b/src/Interface/HasOrder/Instance.agda
@@ -23,3 +23,13 @@ instance
     ⊎.[ <⇒≤ , ≤-reflexive ] }
   ℤ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Int.≤-antisym }
   ℤ-hasDecPartialOrder = HasDecPartialOrder {A = ℤ} ∋ record {}
+
+  open import Data.Rational using (ℚ)
+  import Data.Rational.Properties as Rat hiding (_≟_)
+
+  ℚ-Dec-≤ = ⁇² Rat._≤?_
+  ℚ-Dec-< = ⁇² Rat._<?_
+
+  ℚ-hasPreorder = hasPreorderFromNonStrict Rat.≤-isPreorder _≟_
+  ℚ-hasPartialOrder = HasPartialOrder ∋ record { ≤-antisym = Rat.≤-antisym }
+  ℚ-hasDecPartialOrder = HasDecPartialOrder {A = ℚ} ∋ record {}
diff --git a/src/Prelude.agda b/src/Prelude.agda
index 5c4a7efc8..d7cca55dd 100644
--- a/src/Prelude.agda
+++ b/src/Prelude.agda
@@ -29,7 +29,7 @@ open import Data.Sum public
 open import Data.Product public
   hiding (assocʳ; assocˡ; map; map₁; map₂; map₂′; swap; _<*>_)
 open import Data.Nat public
-  hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_; less-than-or-equal)
+  hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_; _≥_; _>_; less-than-or-equal)
   renaming (_+_ to _+ℕ_)
 open import Data.Integer as ℤ public
   using (ℤ; _⊖_)