Update standard library for better readability, efficiency and iterat…

…or use (#2153)

This does not change any examples or documentation. The interface of the
standard library remains unchanged (except the addition of new
iterators), so this PR can be merged without side effects.

* Closes #2146

tests/Compilation/positive/test028.juvix

@@ -4,8 +4,6 @@ module test028;
 open import Stdlib.Prelude;
 open import Stdlib.Data.Nat.Ord;
 
-type Unit := unit : Unit;
-
 type Stream := cons : Nat → (Unit → Stream) → Stream;
 
 force : (Unit → Stream) → Stream;

tests/Compilation/positive/test054.juvix

@@ -3,35 +3,35 @@ module test054;
 
 import Stdlib.Prelude open;
 
-syntax iterator for;
-for : {A B : Type} → (A → B → A) → A → List B → A;
-for := foldl {_} {_};
+syntax iterator myfor;
+myfor : {A B : Type} → (A → B → A) → A → List B → A;
+myfor := foldl {_} {_};
 
 syntax iterator mymap {init: 0};
 mymap : {A B : Type} → (A → B) → List A → List B;
 mymap f nil := nil;
 mymap f (x :: xs) := f x :: mymap f xs;
 
 sum : List Nat → Nat;
-sum xs := for (acc := 0) (x in xs) acc + x;
+sum xs := myfor (acc := 0) (x in xs) acc + x;
 
 sum' : List Nat → Nat;
-sum' xs := for λ {acc x := acc + x} 0 xs;
+sum' xs := myfor λ {acc x := acc + x} 0 xs;
 
 lst : List Nat;
 lst := 1 :: 2 :: 3 :: 4 :: 5 :: nil;
 
-syntax iterator for2 {init: 1, range: 2};
-for2 :
+syntax iterator myfor2 {init: 1, range: 2};
+myfor2 :
   {A B C : Type}
     → (A → B → C → A)
     → A
     → List B
     → List C
     → A;
-for2 f acc xs ys :=
-  for (acc' := acc) (x in xs)
-    for (acc'' := acc') (y in ys) f acc'' x y;
+myfor2 f acc xs ys :=
+  myfor (acc' := acc) (x in xs)
+    myfor (acc'' := acc') (y in ys) f acc'' x y;
 
 syntax iterator myzip2 {init: 2, range: 2};
 myzip2 :
@@ -43,18 +43,18 @@ myzip2 :
     → List C
     → A × A';
 myzip2 f a b xs ys :=
-  for (acc, acc' := a, b) (x, y in zip xs ys)
+  myfor (acc, acc' := a, b) (x, y in zip xs ys)
     f acc acc' x y;
 
 main : Nat;
 main :=
   sum lst
     + sum' lst
-    + fst (for (a, b := 0, 0) (x in lst) b + x, a)
-    + (for2 (acc := 0) (x in lst; y in 1 :: 2 :: nil)
+    + fst (myfor (a, b := 0, 0) (x in lst) b + x, a)
+    + (myfor2 (acc := 0) (x in lst; y in 1 :: 2 :: nil)
          acc + x + y)
     + fst
       (myzip2 (a := 0; b := 0) (x in lst; y in reverse lst)
          a + x * y, b + y)
-    + for (a := 0) (x, y in mymap (x in lst) x, x + 1)
+    + myfor (a := 0) (x, y in mymap (x in lst) x, x + 1)
         a + x * y;

tests/positive/Reachability/N.juvix

@@ -1,7 +1,7 @@
 module N;
 
 import M open;
-import Stdlib.Prelude open;
+import Stdlib.Prelude open hiding {Unit};
 
 test : {A : Type} -> A -> A;
 test x := x;