From 94874a70648f465b06e754e21286d6782bc7178f Mon Sep 17 00:00:00 2001
From: Michael Heuer <michael.heuer@rwth-aachen.de>
Date: Tue, 8 Oct 2024 14:53:51 +0200
Subject: [PATCH] refactor: implement Ord trait

---
 Anoma/Proving/Types.juvix            |  2 +-
 Anoma/Resource/Computable/Kind.juvix | 15 ++++++++++++++-
 2 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/Anoma/Proving/Types.juvix b/Anoma/Proving/Types.juvix
index 8432715..85e57c3 100644
--- a/Anoma/Proving/Types.juvix
+++ b/Anoma/Proving/Types.juvix
@@ -115,7 +115,7 @@ module ResourceLogic;
 
   module ProofInternal;
     --- Compares two ;Proof; objects.
-    compare (lhs rhs : Proof) : Ordering :=  Ord.cmp (Proof.unProof lhs) (Proof.unProof rhs);
+    compare (lhs rhs : Proof) : Ordering := Ord.cmp (Proof.unProof lhs) (Proof.unProof rhs);
 
     --- Implements the ;Ord; trait for ;Proof;.
     instance
diff --git a/Anoma/Resource/Computable/Kind.juvix b/Anoma/Resource/Computable/Kind.juvix
index b6d98e5..65509f8 100644
--- a/Anoma/Resource/Computable/Kind.juvix
+++ b/Anoma/Resource/Computable/Kind.juvix
@@ -1,7 +1,9 @@
 module Anoma.Resource.Computable.Kind;
 
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
 import Anoma.Resource.Object open using {Resource; module Resource};
-import Anoma.Resource.Types open using {LogicRef; LabelRef; Kind};
+import Anoma.Resource.Types open using {LogicRef; LabelRef; Kind; module Kind};
 import Anoma.Utils open;
 
 module KindInternal;
@@ -9,6 +11,17 @@ module KindInternal;
   --- NOTE: This definition does not specify that the ;LogicRef; and ;LabelRef; arguments
   --- must come from the same ;Resource; although this must be the case.
   kind (logicRef : LogicRef) (labelRef : LabelRef) : Kind := MISSING_ANOMA_BUILTIN;
+
+  --- Compares two ;Kind; objects.
+  compare (lhs rhs : Kind) : Ordering := Ord.cmp (Kind.unKind lhs) (Kind.unKind rhs);
+
+  --- Implements the ;Ord; trait for ;Kind;.
+  instance
+  Kind-Ord : Ord Kind := mkOrd compare;
+
+  --- Implements the ;Eq; trait for ;Kind;.
+  instance
+  Kind-Eq : Eq Kind := fromOrdToEq;
 end;
 
 --- Computes the ;Kind; value of a given ;Resource;.