Skip to content

Commit

Permalink
Update to latest stdlib (#2048)
Browse files Browse the repository at this point in the history
This PR updates the juvix-stdlib submodule. In particular the update
contains the new traits implemented in
anoma/juvix-stdlib#54.

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
  • Loading branch information
paulcadman and janmasrovira authored May 4, 2023
1 parent aace4ca commit 70f27fc
Show file tree
Hide file tree
Showing 6 changed files with 4 additions and 30 deletions.
5 changes: 2 additions & 3 deletions examples/demo/Demo.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ open import Stdlib.Prelude;
-- for comparisons on natural numbers
open import Stdlib.Data.Nat.Ord;
-- for Ordering
open import Stdlib.Data.Ord;

even : Nat → Bool;
even zero := true;
Expand Down Expand Up @@ -40,9 +39,9 @@ terminating
sort : {A : Type} → (A → A → Ordering) → List A → List A;
sort _ nil := nil;
sort _ xs@(_ :: nil) := xs;
sort cmp xs :=
sort {A} cmp xs :=
uncurry
(merge cmp)
(merge (mkOrd cmp))
(both (sort cmp) (splitAt (div (length xs) 2) xs));

printNatListLn : List Nat → IO;
Expand Down
4 changes: 0 additions & 4 deletions examples/milestone/Hanoi/Hanoi.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,6 @@ concat := foldl (++str) "";
intercalate : String → List String → String;
intercalate sep xs := concat (intersperse sep xs);

--- Joins a list of strings with the newline character
unlines : List String → String;
unlines := intercalate "\n";

--- Produce a singleton List
singleton : {A : Type} → A → List A;
singleton a := a :: nil;
Expand Down
16 changes: 0 additions & 16 deletions examples/milestone/PascalsTriangle/PascalsTriangle.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -6,18 +6,6 @@ module PascalsTriangle;

open import Stdlib.Prelude;

zipWith :
{A : Type}
→ {B : Type}
→ {C : Type}
→ (A → B → C)
→ List A
→ List B
→ List C;
zipWith f nil _ := nil;
zipWith f _ nil := nil;
zipWith f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;

--- Return a list of repeated applications of a given function
scanIterate : {A : Type} → Nat → (A → A) → A → List A;
scanIterate zero _ _ := nil;
Expand All @@ -37,10 +25,6 @@ concat := foldl (++str) "";
intercalate : String → List String → String;
intercalate sep xs := concat (intersperse sep xs);

--- Joins a list of strings with the newline character
unlines : List String → String;
unlines := intercalate "\n";

showList : List Nat → String;
showList xs :=
"[" ++str intercalate "," (map natToString xs) ++str "]";
Expand Down
4 changes: 0 additions & 4 deletions examples/milestone/TicTacToe/Logic/Extra.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,3 @@ surround x xs := (x :: intersperse x xs) ++ x :: nil;
--- It inserts the first ;String; in between the ;String;s in the second list and concatenates the result
intercalate : String → List String → String;
intercalate sep xs := concat (intersperse sep xs);

--- Joins a list of strings with the newline character
unlines : List String → String;
unlines := intercalate "\n";
3 changes: 1 addition & 2 deletions tests/Internal/positive/QuickSort.juvix
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
module QuickSort;

open import Stdlib.Prelude;
open import Stdlib.Prelude hiding {quickSort};
open import Stdlib.Data.Nat.Ord;
open import Stdlib.Data.Ord;

qsHelper : {A : Type} → A → List A × List A → List A;
qsHelper a (l , r) := l ++ (a :: nil) ++ r;
Expand Down

0 comments on commit 70f27fc

Please sign in to comment.