From 7260952158e18a02016ecee5bbe4715b2a761642 Mon Sep 17 00:00:00 2001
From: whatisRT <andre.knispel@gmx.de>
Date: Thu, 7 Dec 2023 11:49:49 +0100
Subject: [PATCH] Add order instances for rational numbers

---
 Class/Decidable/Instances.agda | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Class/Decidable/Instances.agda b/Class/Decidable/Instances.agda
index 8e060e6..567afe8 100644
--- a/Class/Decidable/Instances.agda
+++ b/Class/Decidable/Instances.agda
@@ -101,3 +101,8 @@ instance
 
   ℤ-Dec-≤ = ⁇² ℤ._≤?_
   ℤ-Dec-< = ⁇² ℤ._<?_
+
+  import Data.Rational.Properties as Rat
+
+  ℚ-Dec-≤ = ⁇² Rat._≤?_
+  ℚ-Dec-< = ⁇² Rat._<?_