From 09853c7d078ae575b33dcb49f0d4bed35e8820dd Mon Sep 17 00:00:00 2001
From: Aleksander Wolska <odderwiser@gmail.com>
Date: Wed, 25 Dec 2024 20:09:11 +0100
Subject: [PATCH] iLwfulOrd Char

---
 lib/Haskell/Law/Ord/Char.agda | 68 +++++++++++++++++++++++++++++++++++
 lib/Haskell/Law/Ord/Def.agda  |  2 --
 2 files changed, 68 insertions(+), 2 deletions(-)
 create mode 100644 lib/Haskell/Law/Ord/Char.agda

diff --git a/lib/Haskell/Law/Ord/Char.agda b/lib/Haskell/Law/Ord/Char.agda
new file mode 100644
index 00000000..1af05afc
--- /dev/null
+++ b/lib/Haskell/Law/Ord/Char.agda
@@ -0,0 +1,68 @@
+module Haskell.Law.Ord.Char where
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+open import Haskell.Prim.Ord
+
+open import Haskell.Law.Bool
+open import Haskell.Law.Eq.Def
+open import Haskell.Law.Eq.Instances
+open import Haskell.Law.Ord.Def
+open import Haskell.Law.Ord.Nat
+
+instance
+  iLawfulOrdChar : IsLawfulOrd Char
+
+  iLawfulOrdChar .comparability a b 
+    with (c2n a) | (c2n b) 
+  ... | n | m = comparability n m
+
+  iLawfulOrdChar .transitivity a b c h 
+    with (c2n a) | (c2n b) | (c2n c)
+  ... | n | m | o = transitivity n m o h
+
+  iLawfulOrdChar .reflexivity a
+    with (c2n a)
+  ... | n = reflexivity n
+
+  iLawfulOrdChar .antisymmetry a b h
+    with (c2n a) | (c2n b)
+  ... | n | m = antisymmetry n m h
+  
+  iLawfulOrdChar .lte2gte a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = lte2gte n m
+
+  iLawfulOrdChar .lt2LteNeq a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = lt2LteNeq n m
+
+  iLawfulOrdChar .lt2gt a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = lt2gt n m
+
+  iLawfulOrdChar .compareLt a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = compareLt n m
+
+  iLawfulOrdChar .compareGt a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = compareGt n m
+
+  iLawfulOrdChar .compareEq a b 
+    with (c2n a) | (c2n b)
+  ... | n | m = compareEq n m
+
+  iLawfulOrdChar .min2if a b 
+    with (c2n a) | (c2n b)
+  ... | n | m 
+    rewrite lte2ngt n m 
+    | ifFlip (m < n) a b 
+    = eqReflexivity (if (m < n) then b else a) 
+
+  iLawfulOrdChar .max2if a b
+    with (c2n a) | (c2n b)
+  ... | n | m 
+    rewrite gte2nlt n m
+    | ifFlip (n < m) a b  
+    = eqReflexivity (if (n < m) then b else a)
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index ab153c54..73b5f387 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/lib/Haskell/Law/Ord/Def.agda
@@ -178,8 +178,6 @@ postulate instance
 
   iLawfulOrdDouble : IsLawfulOrd Double
 
-  iLawfulOrdChar : IsLawfulOrd Char
-
   iLawfulOrdUnit : IsLawfulOrd ⊤
 
   iLawfulOrdTuple₂ : ⦃ iOrdA : Ord a ⦄ ⦃ iOrdB : Ord b ⦄