refactor: implement Ord trait

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

Anoma/Resource/Computable/Kind.juvix

@@ -1,14 +1,27 @@
 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;
   --- The kind function as defined in the RM specs.
   --- 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;.