Use instance fields to make Natural into a FromNatural

anoma · Jul 31, 2024 · 57964c6 · 57964c6
1 parent dad5c1a
commit 57964c6
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/include/package-base/Juvix/Builtin/V1/Nat.juvix b/include/package-base/Juvix/Builtin/V1/Nat.juvix
@@ -1,14 +1,21 @@
 module Juvix.Builtin.V1.Nat;
 
 import Juvix.Builtin.V1.Trait.Natural open public;
+import Juvix.Builtin.V1.Trait.FromNatural open public;
 import Juvix.Builtin.V1.Nat.Base open hiding {+; *; div; mod} public;
 import Juvix.Builtin.V1.Nat.Base as Nat;
 
+{-# specialize: true, inline: case #-}
+instance
+fromNaturalNatI : FromNatural Nat :=
+  mkFromNatural@{
+    fromNat (x : Nat) : Nat := x
+  };
+
 {-# specialize: true, inline: case #-}
 instance
 naturalNatI : Natural Nat :=
   mkNatural@{
     + := (Nat.+);
     * := (Nat.*);
-    fromNat (x : Nat) : Nat := x
   };
diff --git a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
@@ -7,20 +7,13 @@ import Juvix.Builtin.V1.Trait.FromNatural open;
 trait
 type Natural A :=
   mkNatural {
+    {{FromNaturalI}} : FromNatural A;
     syntax operator + additive;
     {-# isabelle-operator: {name: "+", prec: 65, assoc: left} #-}
     + : A -> A -> A;
     syntax operator * multiplicative;
     {-# isabelle-operator: {name: "*", prec: 70, assoc: left} #-}
     * : A -> A -> A;
-    fromNat : Nat -> A
   };
 
 open Natural public;
-
-{-# specialize: true, inline: case #-}
-coercion instance
-fromNaturalNatI {A} {{Natural A}} : FromNatural A :=
-  mkFromNatural@{
-    fromNat := Natural.fromNat
-  };