Add general Natural -> FromNatural coercion with specialize pragma

anoma · Jul 30, 2024 · 968db25 · 968db25
1 parent 2025370
commit 968db25
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix b/include/package-base/Juvix/Builtin/V1/Trait/Natural.juvix
@@ -18,5 +18,9 @@ type Natural A :=
 
 open Natural public;
 
+{-# specialize: true, inline: case #-}
 coercion instance
-FromNaturalNaturalI {A} {{N : Natural A}} : FromNatural A := mkFromNatural@{fromNat};
+fromNaturalNatI {A} {{Natural A}} : FromNatural A :=
+  mkFromNatural@{
+    fromNat := Natural.fromNat
+  };