From 2adb9df345be4c6b217d9fa06ca5ef4410a7cd79 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 14 Nov 2024 15:29:14 +0100
Subject: [PATCH 1/7] make Eq builtin

---
 Stdlib/Trait/Eq.juvix | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
index 71cb707f..fe3d7c7f 100644
--- a/Stdlib/Trait/Eq.juvix
+++ b/Stdlib/Trait/Eq.juvix
@@ -4,8 +4,9 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.Fixity open;
 
 --- A trait defining equality
+builtin eq
 trait
-type Eq A := mkEq@{eq : A -> A -> Bool};
+type Eq A := mkEq@{builtin isEqual eq : A -> A -> Bool};
 
 syntax operator == comparison;
 syntax operator /= comparison;

From d5ea0a56115810ad31e2489de54e1a25980eaa00 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 20 Nov 2024 08:24:22 +0100
Subject: [PATCH 2/7] derive some Eq instances

---
 Stdlib/Data/Bool.juvix   | 11 ++---------
 Stdlib/Data/Maybe.juvix  | 11 ++---------
 Stdlib/Data/Pair.juvix   |  9 ++-------
 Stdlib/Data/Result.juvix | 11 ++---------
 Stdlib/Data/Unit.juvix   |  7 ++-----
 Stdlib/Trait/Ord.juvix   | 11 ++---------
 6 files changed, 12 insertions(+), 48 deletions(-)

diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix
index 73490d07..6b275e43 100644
--- a/Stdlib/Data/Bool.juvix
+++ b/Stdlib/Data/Bool.juvix
@@ -8,15 +8,8 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqBoolI : Eq Bool :=
-  mkEq@{
-    eq (x y : Bool) : Bool :=
-      case x, y of
-        | true, true := true
-        | false, false := true
-        | _ := false;
-  };
+deriving instance
+eqBoolI : Eq Bool;
 
 {-# specialize: true, inline: case #-}
 instance
diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
index 2fff90d6..25103e62 100644
--- a/Stdlib/Data/Maybe.juvix
+++ b/Stdlib/Data/Maybe.juvix
@@ -14,15 +14,8 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Data.Pair.Base open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
-  mkEq@{
-    eq (m1 m2 : Maybe A) : Bool :=
-      case m1, m2 of
-        | nothing, nothing := true
-        | just a1, just a2 := Eq.eq a1 a2
-        | _ := false;
-  };
+deriving instance
+eqMaybeI {A} {{Eq A}} : Eq (Maybe A);
 
 instance
 showMaybeI {A} {{Show A}} : Show (Maybe A) :=
diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix
index bcadcc76..fcf6a17e 100644
--- a/Stdlib/Data/Pair.juvix
+++ b/Stdlib/Data/Pair.juvix
@@ -9,13 +9,8 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
-instance
-eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
-  | {{mkEq eqA}} {{mkEq eqB}} :=
-    mkEq@{
-      eq (p1 p2 : Pair A B) : Bool :=
-        case p1, p2 of (a1, b1), a2, b2 := eqA a1 a2 && eqB b1 b2;
-    };
+deriving instance
+eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);
 
 {-# specialize: true, inline: case #-}
 instance
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index 8da00279..a836b286 100644
--- a/Stdlib/Data/Result.juvix
+++ b/Stdlib/Data/Result.juvix
@@ -24,15 +24,8 @@ ordResultI
   };
 
 {-# specialize: true, inline: case #-}
-instance
-eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) :=
-  mkEq@{
-    eq (result1 result2 : Result Error Value) : Bool :=
-      case result1, result2 of
-        | error a1, error a2 := a1 == a2
-        | ok b1, ok b2 := b1 == b2
-        | _, _ := false;
-  };
+deriving instance
+eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value);
 
 instance
 showResultI
diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix
index 1bdb887c..a719b592 100644
--- a/Stdlib/Data/Unit.juvix
+++ b/Stdlib/Data/Unit.juvix
@@ -10,11 +10,8 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Foldable open;
 
-instance
-eqUnitI : Eq Unit :=
-  mkEq@{
-    eq (_ _ : Unit) : Bool := true;
-  };
+deriving instance
+eqUnitI : Eq Unit;
 
 instance
 ordUnitI : Ord Unit :=
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index d590a868..c55ab9e8 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -24,15 +24,8 @@ isGreaterThan (ordering : Ordering) : Bool :=
     | GreaterThan := true
     | _ := false;
 
-instance
-orderingEqI : Eq Ordering :=
-  mkEq@{
-    eq (ordering1 ordering2 : Ordering) : Bool :=
-      case ordering2 of
-        | LessThan := isLessThan ordering1
-        | Equal := isEqual ordering1
-        | GreaterThan := isGreaterThan ordering1;
-  };
+deriving instance
+orderingEqI : Eq Ordering;
 
 --- A trait for defining a total order
 trait

From 09c0bb7c0acea71fdca18adf835c5d13c380e0ea Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 21 Nov 2024 19:47:56 +0100
Subject: [PATCH 3/7] derive some Ord instances

---
 Stdlib/Data/Bool.juvix   | 12 ++----------
 Stdlib/Data/Maybe.juvix  | 12 ++----------
 Stdlib/Data/Pair.juvix   | 14 ++------------
 Stdlib/Data/Result.juvix | 12 ++----------
 Stdlib/Data/Unit.juvix   |  7 ++-----
 Stdlib/Trait/Ord.juvix   |  7 ++++++-
 6 files changed, 16 insertions(+), 48 deletions(-)

diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix
index 6b275e43..af191c98 100644
--- a/Stdlib/Data/Bool.juvix
+++ b/Stdlib/Data/Bool.juvix
@@ -12,16 +12,8 @@ deriving instance
 eqBoolI : Eq Bool;
 
 {-# specialize: true, inline: case #-}
-instance
-ordBoolI : Ord Bool :=
-  mkOrd@{
-    cmp (x y : Bool) : Ordering :=
-      case x, y of
-        | false, false := Equal
-        | false, true := LessThan
-        | true, false := GreaterThan
-        | true, true := Equal;
-  };
+deriving instance
+ordBoolI : Ord Bool;
 
 instance
 showBoolI : Show Bool :=
diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
index 25103e62..f2fe5036 100644
--- a/Stdlib/Data/Maybe.juvix
+++ b/Stdlib/Data/Maybe.juvix
@@ -27,16 +27,8 @@ showMaybeI {A} {{Show A}} : Show (Maybe A) :=
   };
 
 {-# specialize: true, inline: case #-}
-instance
-ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
-  mkOrd@{
-    cmp (m1 m2 : Maybe A) : Ordering :=
-      case m1, m2 of
-        | nothing, nothing := Equal
-        | just a1, just a2 := Ord.cmp a1 a2
-        | nothing, just _ := LessThan
-        | just _, nothing := GreaterThan;
-  };
+deriving instance
+ordMaybeI {A} {{Ord A}} : Ord (Maybe A);
 
 {-# specialize: true, inline: case #-}
 instance
diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix
index fcf6a17e..76fdd832 100644
--- a/Stdlib/Data/Pair.juvix
+++ b/Stdlib/Data/Pair.juvix
@@ -13,18 +13,8 @@ deriving instance
 eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);
 
 {-# specialize: true, inline: case #-}
-instance
-ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
-  | {{mkOrd cmpA}} {{mkOrd cmpB}} :=
-    mkOrd@{
-      cmp (p1 p2 : Pair A B) : Ordering :=
-        case p1, p2 of
-          (a1, b1), a2, b2 :=
-            case cmpA a1 a2 of
-              | LessThan := LessThan
-              | GreaterThan := GreaterThan
-              | Equal := cmpB b1 b2;
-    };
+deriving instance
+ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B);
 
 instance
 showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index a836b286..2f6245ad 100644
--- a/Stdlib/Data/Result.juvix
+++ b/Stdlib/Data/Result.juvix
@@ -11,17 +11,9 @@ import Stdlib.Trait.Show open;
 import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
-instance
+deriving instance
 ordResultI
-  {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) :=
-  mkOrd@{
-    cmp (result1 result2 : Result Error Value) : Ordering :=
-      case result1, result2 of
-        | error a1, error a2 := Ord.cmp a1 a2
-        | ok b1, ok b2 := Ord.cmp b1 b2
-        | error _, ok _ := LessThan
-        | ok _, error _ := GreaterThan;
-  };
+  {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value);
 
 {-# specialize: true, inline: case #-}
 deriving instance
diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix
index a719b592..c004f780 100644
--- a/Stdlib/Data/Unit.juvix
+++ b/Stdlib/Data/Unit.juvix
@@ -13,11 +13,8 @@ import Stdlib.Trait.Foldable open;
 deriving instance
 eqUnitI : Eq Unit;
 
-instance
-ordUnitI : Ord Unit :=
-  mkOrd@{
-    cmp (_ _ : Unit) : Ordering := Equal;
-  };
+deriving instance
+ordUnitI : Ord Unit;
 
 instance
 showUnitI : Show Unit :=
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index c55ab9e8..d1222b6e 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -4,6 +4,7 @@ import Stdlib.Data.Fixity open;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Trait.Eq open;
 
+builtin ordering
 type Ordering :=
   | LessThan
   | Equal
@@ -28,8 +29,12 @@ deriving instance
 orderingEqI : Eq Ordering;
 
 --- A trait for defining a total order
+builtin ord
 trait
-type Ord A := mkOrd@{cmp : A -> A -> Ordering};
+type Ord A := mkOrd@{builtin compare cmp : A -> A -> Ordering};
+
+deriving instance
+orderingOrdI : Ord Ordering;
 
 syntax operator <= comparison;
 

From 9534bd214df2983f4f5918ddcff3703f63bd1de1 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 22 Nov 2024 10:00:22 +0100
Subject: [PATCH 4/7] move Ordering to its own module

---
 Stdlib/Data/Ordering.juvix | 38 ++++++++++++++++++++++++++++++++++++++
 Stdlib/Trait/Ord.juvix     | 25 +------------------------
 Stdlib/Trait/Show.juvix    |  2 +-
 3 files changed, 40 insertions(+), 25 deletions(-)
 create mode 100644 Stdlib/Data/Ordering.juvix

diff --git a/Stdlib/Data/Ordering.juvix b/Stdlib/Data/Ordering.juvix
new file mode 100644
index 00000000..b399d754
--- /dev/null
+++ b/Stdlib/Data/Ordering.juvix
@@ -0,0 +1,38 @@
+module Stdlib.Data.Ordering;
+
+import Stdlib.Trait.Eq open;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Trait.Show open;
+
+builtin ordering
+type Ordering :=
+  | LessThan
+  | Equal
+  | GreaterThan;
+
+isLessThan (ordering : Ordering) : Bool :=
+  case ordering of
+    | LessThan := true
+    | _ := false;
+
+isEqual (ordering : Ordering) : Bool :=
+  case ordering of
+    | Equal := true
+    | _ := false;
+
+isGreaterThan (ordering : Ordering) : Bool :=
+  case ordering of
+    | GreaterThan := true
+    | _ := false;
+
+deriving instance
+orderingEqI : Eq Ordering;
+
+instance
+orderingShowI : Show Ordering :=
+  mkShow@{
+    show : Ordering -> String
+      | Equal := "Equal"
+      | LessThan := "LessThan"
+      | GreaterThan := "GreaterThan";
+  };
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index d1222b6e..f79a5ee4 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -3,30 +3,7 @@ module Stdlib.Trait.Ord;
 import Stdlib.Data.Fixity open;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Trait.Eq open;
-
-builtin ordering
-type Ordering :=
-  | LessThan
-  | Equal
-  | GreaterThan;
-
-isLessThan (ordering : Ordering) : Bool :=
-  case ordering of
-    | LessThan := true
-    | _ := false;
-
-isEqual (ordering : Ordering) : Bool :=
-  case ordering of
-    | Equal := true
-    | _ := false;
-
-isGreaterThan (ordering : Ordering) : Bool :=
-  case ordering of
-    | GreaterThan := true
-    | _ := false;
-
-deriving instance
-orderingEqI : Eq Ordering;
+import Stdlib.Data.Ordering open public;
 
 --- A trait for defining a total order
 builtin ord
diff --git a/Stdlib/Trait/Show.juvix b/Stdlib/Trait/Show.juvix
index 099513b0..07319430 100644
--- a/Stdlib/Trait/Show.juvix
+++ b/Stdlib/Trait/Show.juvix
@@ -1,6 +1,6 @@
 module Stdlib.Trait.Show;
 
-import Stdlib.Data.String.Base open;
+import Juvix.Builtin.V1.String open public;
 
 trait
 type Show A := mkShow@{show : A -> String};

From fde9ac23534fe1c0ba3f69714233dbd1d3934a9c Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Fri, 29 Nov 2024 09:47:50 +0100
Subject: [PATCH 5/7] format

---
 Stdlib/Data/Result.juvix   | 3 +--
 Stdlib/Trait/Eq.juvix      | 6 +++++-
 Stdlib/Trait/Ord.juvix     | 6 +++++-
 Stdlib/Trait/Partial.juvix | 5 ++++-
 Stdlib/Trait/Show.juvix    | 5 ++++-
 5 files changed, 19 insertions(+), 6 deletions(-)

diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index 2f6245ad..ad2eb1e9 100644
--- a/Stdlib/Data/Result.juvix
+++ b/Stdlib/Data/Result.juvix
@@ -12,8 +12,7 @@ import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
 deriving instance
-ordResultI
-  {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value);
+ordResultI {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value);
 
 {-# specialize: true, inline: case #-}
 deriving instance
diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
index fe3d7c7f..1f0ce368 100644
--- a/Stdlib/Trait/Eq.juvix
+++ b/Stdlib/Trait/Eq.juvix
@@ -6,7 +6,11 @@ import Stdlib.Data.Fixity open;
 --- A trait defining equality
 builtin eq
 trait
-type Eq A := mkEq@{builtin isEqual eq : A -> A -> Bool};
+type Eq A :=
+  mkEq@{
+    builtin isEqual
+    eq : A -> A -> Bool;
+  };
 
 syntax operator == comparison;
 syntax operator /= comparison;
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index f79a5ee4..a8627de5 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -8,7 +8,11 @@ import Stdlib.Data.Ordering open public;
 --- A trait for defining a total order
 builtin ord
 trait
-type Ord A := mkOrd@{builtin compare cmp : A -> A -> Ordering};
+type Ord A :=
+  mkOrd@{
+    builtin compare
+    cmp : A -> A -> Ordering;
+  };
 
 deriving instance
 orderingOrdI : Ord Ordering;
diff --git a/Stdlib/Trait/Partial.juvix b/Stdlib/Trait/Partial.juvix
index 1670c417..ff57bdc9 100644
--- a/Stdlib/Trait/Partial.juvix
+++ b/Stdlib/Trait/Partial.juvix
@@ -4,7 +4,10 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Debug.Fail as Debug;
 
 trait
-type Partial := mkPartial@{fail : {A : Type} -> String -> A};
+type Partial :=
+  mkPartial@{
+    fail : {A : Type} -> String -> A;
+  };
 
 open Partial public;
 
diff --git a/Stdlib/Trait/Show.juvix b/Stdlib/Trait/Show.juvix
index 07319430..9ca64c21 100644
--- a/Stdlib/Trait/Show.juvix
+++ b/Stdlib/Trait/Show.juvix
@@ -3,4 +3,7 @@ module Stdlib.Trait.Show;
 import Juvix.Builtin.V1.String open public;
 
 trait
-type Show A := mkShow@{show : A -> String};
+type Show A :=
+  mkShow@{
+    show : A -> String;
+  };

From 0c456725a23648606f97aebf8f74a9e2a73e90b6 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 29 Nov 2024 12:14:21 +0100
Subject: [PATCH 6/7] more pragmas

---
 Stdlib/Data/List.juvix                  | 6 ++++--
 Stdlib/Data/Map.juvix                   | 1 +
 Stdlib/Trait/Foldable/Monomorphic.juvix | 2 +-
 Stdlib/Trait/Functor/Monomorphic.juvix  | 2 +-
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
index f62aa06d..fb72292a 100644
--- a/Stdlib/Data/List.juvix
+++ b/Stdlib/Data/List.juvix
@@ -21,6 +21,7 @@ phead {A} {{Partial}} : List A -> A
   | (x :: _) := x
   | nil := fail "head: empty list";
 
+{-# specialize: true, inline: case #-}
 instance
 eqListI {A} {{Eq A}} : Eq (List A) :=
   let
@@ -37,6 +38,7 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
 isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool :=
   isElement (Eq.eq) elem list;
 
+{-# specialize: true, inline: case #-}
 instance
 ordListI {A} {{Ord A}} : Ord (List A) :=
   let
@@ -71,7 +73,7 @@ functorListI : Functor List :=
     map := listMap;
   };
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: case #-}
 instance
 monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A :=
   fromPolymorphicFunctor;
@@ -84,7 +86,7 @@ polymorphicFoldableListI : Polymorphic.Foldable List :=
     rfor := listRfor;
   };
 
-{-# specialize: true, inline: true #-}
+{-# specialize: true, inline: case #-}
 instance
 foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
 
diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix
index 75ee1f53..16a598c5 100644
--- a/Stdlib/Data/Map.juvix
+++ b/Stdlib/Data/Map.juvix
@@ -32,6 +32,7 @@ value {Key Value} (binding : Binding Key Value) : Value :=
 toPair {Key Value} (binding : Binding Key Value) : Pair Key Value :=
   key binding, value binding;
 
+{-# specialize: true, inline: case #-}
 instance
 bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) :=
   mkOrd@{
diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
index da38c701..5bdd161e 100644
--- a/Stdlib/Trait/Foldable/Monomorphic.juvix
+++ b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -19,7 +19,7 @@ open Foldable public;
 
 --- Make a monomorphic ;Foldable; instance from a polymorphic one.
 --- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance.
-{-# inline: case #-}
+{-# inline: always #-}
 fromPolymorphicFoldable
   {F : Type -> Type}
   {{foldable : Poly.Foldable F}}
diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix
index 076fde2c..4dd92fc6 100644
--- a/Stdlib/Trait/Functor/Monomorphic.juvix
+++ b/Stdlib/Trait/Functor/Monomorphic.juvix
@@ -15,7 +15,7 @@ type Functor (Container Elem : Type) :=
 
 open Functor public;
 
-{-# inline: case #-}
+{-# inline: always #-}
 fromPolymorphicFunctor
   {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem :=
   mkFunctor@{

From 561425ecb3bca7d6c8ec6b4f93932510597c4c59 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 2 Dec 2024 16:02:27 +0100
Subject: [PATCH 7/7] Add qualified Nat and Int modules

---
 Stdlib/Data/Field.juvix |  2 +-
 Stdlib/Data/Int.juvix   | 14 ++++++++------
 Stdlib/Data/Nat.juvix   | 17 ++++++++++-------
 3 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/Stdlib/Data/Field.juvix b/Stdlib/Data/Field.juvix
index b11c5fae..ab73bbf9 100644
--- a/Stdlib/Data/Field.juvix
+++ b/Stdlib/Data/Field.juvix
@@ -1,7 +1,7 @@
 module Stdlib.Data.Field;
 
 import Stdlib.Data.Field.Base open using {Field} public;
-import Stdlib.Data.Field.Base as Field;
+import Stdlib.Data.Field.Base as Field public;
 import Stdlib.Data.String.Base open;
 import Stdlib.Data.Nat;
 
diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
index cf62bf77..f634e777 100644
--- a/Stdlib/Data/Int.juvix
+++ b/Stdlib/Data/Int.juvix
@@ -1,8 +1,13 @@
 module Stdlib.Data.Int;
 
-import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public;
--- should be re-exported qualified
-import Stdlib.Data.Int.Base as Int;
+import Stdlib.Data.Int.Base open hiding {module Int; +; -; *; div; mod} public;
+
+module Int;
+  open Stdlib.Data.Int.Base.Int public;
+
+  import Stdlib.Data.Int.Base open public;
+  import Stdlib.Data.Int.Ord open public;
+end;
 
 import Stdlib.Data.String open;
 import Stdlib.Data.Bool open;
@@ -15,9 +20,6 @@ import Stdlib.Trait.FromNatural open;
 import Stdlib.Trait.Integral open;
 import Stdlib.Trait.DivMod open;
 
--- should be re-exported qualified
-import Stdlib.Data.Int.Ord as Int;
-
 --- Converts an ;Int; into ;String;.
 builtin int-to-string
 axiom intToString : Int -> String;
diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
index 81d45d07..17ea6af1 100644
--- a/Stdlib/Data/Nat.juvix
+++ b/Stdlib/Data/Nat.juvix
@@ -1,9 +1,15 @@
 module Stdlib.Data.Nat;
 
-import Juvix.Builtin.V1.Nat open public;
-import Stdlib.Data.Nat.Base open hiding {+; *; div; mod} public;
--- should be re-exported qualified
-import Stdlib.Data.Nat.Base as Nat;
+import Juvix.Builtin.V1.Nat open hiding {module Nat} public;
+import Stdlib.Data.Nat.Base open hiding {module Nat; +; *; div; mod} public;
+
+module Nat;
+  open Stdlib.Data.Nat.Base.Nat public;
+
+  import Stdlib.Data.Nat.Base open public;
+  import Stdlib.Data.Nat.Ord open public;
+end;
+
 import Stdlib.Data.String.Base open;
 
 import Stdlib.Trait.Eq open public;
@@ -13,9 +19,6 @@ import Stdlib.Trait.Natural open public;
 import Stdlib.Trait.FromNatural open public;
 import Stdlib.Trait.DivMod open public;
 
--- should be re-exported qualified
-import Stdlib.Data.Nat.Ord as Nat;
-
 --- Converts a ;Nat; into a ;String;.
 builtin nat-to-string
 axiom natToString : Nat -> String;