literal casting

anoma · Oct 23, 2023 · 708d920 · 708d920
1 parent 31b69ed
commit 708d920
Show file tree

Hide file tree

Showing 5 changed files with 14 additions and 12 deletions.
diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix
@@ -6,6 +6,7 @@ import Stdlib.Data.Int.Base open;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering};
 
+import Stdlib.Data.Nat.Base as Nat;
 import Stdlib.Data.Nat.Ord as Nat;
 
 syntax operator == comparison;
@@ -32,7 +33,7 @@ syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
 builtin int-lt
-< (m n : Int) : Bool := m + 1 <= n;
+< (m n : Int) : Bool := m + ofNat (Nat.suc Nat.zero) <= n;
 
 syntax operator > comparison;
 

diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
@@ -5,6 +5,7 @@ import Stdlib.Data.Fixity open;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Trait.Natural open;
 import Stdlib.Trait.Ord open;
+import Stdlib.Data.Nat open;
 
 --- A range of naturals
 type Range N :=
@@ -32,7 +33,7 @@ syntax operator to range;
 --- `x to y` is the range [x..y]
 {-# inline: always #-}
 to {N} {{Natural N}} (l h : N) : Range N :=
-  mkRange l h (fromNat 1);
+  mkRange l h 1;
 
 syntax operator step step;
 

diff --git a/Stdlib/Data/String.juvix b/Stdlib/Data/String.juvix
@@ -1,21 +1,12 @@
 module Stdlib.Data.String;
 
 import Stdlib.Data.String.Base open public;
-import Stdlib.Data.List.Base open;
-import Stdlib.Function open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Show open;
 
 import Stdlib.Data.String.Ord as String;
 
---- Concatenates a ;List; of ;String;s.
-concatStr : List String -> String := foldl (++str) "";
-
---- Joins a ;List; of ;String;s with "\n".
-unlines : List String -> String :=
-  concatStr ∘ intersperse "\n";
-
 instance
 eqStringI : Eq String := mkEq (String.==);
 

diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix
@@ -1,5 +1,7 @@
 module Stdlib.Data.String.Base;
 
+import Stdlib.Data.List.Base open;
+import Stdlib.Function open;
 import Stdlib.Data.Fixity open;
 
 --- Primitive representation of a sequence of characters.
@@ -10,3 +12,10 @@ syntax operator ++str cons;
 --- Concatenation of two ;String;s.
 builtin string-concat
 axiom ++str : String -> String -> String;
+
+--- Concatenates a ;List; of ;String;s.
+concatStr : List String -> String := foldl (++str) "";
+
+--- Joins a ;List; of ;String;s with "\n".
+unlines : List String -> String :=
+  concatStr ∘ intersperse "\n";
diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix
@@ -12,5 +12,5 @@ gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} (a b : A) : A :=
     -- should be smaller than the second.
     terminating
     gcd' (a b : A) : A :=
-      if (a == fromNat 0) b (gcd' (mod b a) a);
+      if (a == 0) b (gcd' (mod b a) a);
   in if (a > b) (gcd' b a) (gcd' a b);