From 70f27fcede82c9af991a8c6cf18594addb6c3bd5 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Thu, 4 May 2023 16:49:10 +0100
Subject: [PATCH] Update to latest stdlib (#2048)

This PR updates the juvix-stdlib submodule. In particular the update
contains the new traits implemented in
https://github.com/anoma/juvix-stdlib/pull/54.

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
---
 examples/demo/Demo.juvix                         |  5 ++---
 examples/milestone/Hanoi/Hanoi.juvix             |  4 ----
 .../PascalsTriangle/PascalsTriangle.juvix        | 16 ----------------
 examples/milestone/TicTacToe/Logic/Extra.juvix   |  4 ----
 juvix-stdlib                                     |  2 +-
 tests/Internal/positive/QuickSort.juvix          |  3 +--
 6 files changed, 4 insertions(+), 30 deletions(-)

diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix
index d854c05b36..a7ecda9dbd 100644
--- a/examples/demo/Demo.juvix
+++ b/examples/demo/Demo.juvix
@@ -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;
@@ -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;
diff --git a/examples/milestone/Hanoi/Hanoi.juvix b/examples/milestone/Hanoi/Hanoi.juvix
index 1793d01c53..649150ba22 100644
--- a/examples/milestone/Hanoi/Hanoi.juvix
+++ b/examples/milestone/Hanoi/Hanoi.juvix
@@ -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;
diff --git a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
index 60dc3add19..6812e8a98c 100644
--- a/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
+++ b/examples/milestone/PascalsTriangle/PascalsTriangle.juvix
@@ -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;
@@ -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 "]";
diff --git a/examples/milestone/TicTacToe/Logic/Extra.juvix b/examples/milestone/TicTacToe/Logic/Extra.juvix
index 34fc662a37..664026c5b5 100644
--- a/examples/milestone/TicTacToe/Logic/Extra.juvix
+++ b/examples/milestone/TicTacToe/Logic/Extra.juvix
@@ -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";
diff --git a/juvix-stdlib b/juvix-stdlib
index 059d502b1f..c3f0ec0f3e 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 059d502b1f989faed5470271e97571c2b1deaa10
+Subproject commit c3f0ec0f3e64bbaee503e4514164087b1b7fe705
diff --git a/tests/Internal/positive/QuickSort.juvix b/tests/Internal/positive/QuickSort.juvix
index 7f2dff35a2..275bee3a5a 100644
--- a/tests/Internal/positive/QuickSort.juvix
+++ b/tests/Internal/positive/QuickSort.juvix
@@ -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;