Rename if to ite (#104)

- We rename `if` to `ite` since `if` will become a keyword in
anoma/juvix#2852

Stdlib/Data/Bool/Base.juvix

@@ -26,7 +26,7 @@ builtin bool-and
 
 --- Returns the first argument if ;true;, otherwise it returns the second argument. Evaluated lazily. Cannot be partially applied.
 builtin bool-if
-if : {A : Type} → Bool → A → A → A
+ite : {A : Type} → Bool → A → A → A
   | true a _ := a
   | false _ b := b;
 

Stdlib/Data/Int/Ord.juvix

@@ -54,7 +54,7 @@ compare (m n : Int) : Ordering :=
     | else := GT;
 
 --- Returns the smallest ;Int;.
-min (x y : Int) : Int := if (x < y) x y;
+min (x y : Int) : Int := ite (x < y) x y;
 
 --- Returns the biggest ;Int;.
-max (x y : Int) : Int := if (x > y) x y;
+max (x y : Int) : Int := ite (x > y) x y;

Stdlib/Data/List.juvix

@@ -21,7 +21,7 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
       | nil nil := true
       | nil _ := false
       | _ nil := false
-      | (x :: xs) (y :: ys) := if (Eq.eq x y) (go xs ys) false;
+      | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false;
   in mkEq go;
 
 instance

Stdlib/Data/List/Base.juvix

@@ -55,7 +55,7 @@ syntax iterator filter {init := 0; range := 1};
 {-# specialize: [1] #-}
 filter {A} (f : A → Bool) : List A → List A
   | nil := nil
-  | (h :: hs) := if (f h) (h :: filter f hs) (filter f hs);
+  | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs);
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
 length {A} (l : List A) : Nat :=
@@ -106,7 +106,7 @@ partition
   | nil := nil, nil
   | (x :: xs) :=
     case partition f xs of
-      l1, l2 := if (f x) (x :: l1, l2) (l1, x :: l2);
+      l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2);
 
 syntax operator ++ cons;
 
@@ -147,15 +147,15 @@ syntax iterator any {init := 0; range := 1};
 {-# specialize: [1] #-}
 any {A} (f : A → Bool) : List A → Bool
   | nil := false
-  | (x :: xs) := if (f x) true (any f xs);
+  | (x :: xs) := ite (f x) true (any f xs);
 
 syntax iterator all {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if all elements of the ;List; satisfy the predicate.
 {-# specialize: [1] #-}
 all {A} (f : A -> Bool) : List A -> Bool
   | nil := true
-  | (x :: xs) := if (f x) (all f xs) false;
+  | (x :: xs) := ite (f x) (all f xs) false;
 
 --- 𝒪(1). Returns ;true; if the ;List; is empty.
 null {A} : List A → Bool

Stdlib/Data/Nat/Ord.juvix

@@ -55,7 +55,7 @@ compare (n m : Nat) : Ordering :=
     | else := GT;
 
 --- Returns the smaller ;Nat;.
-min (x y : Nat) : Nat := if (x < y) x y;
+min (x y : Nat) : Nat := ite (x < y) x y;
 
 --- Returns the larger ;Nat;.
-max (x y : Nat) : Nat := if (x > y) x y;
+max (x y : Nat) : Nat := ite (x > y) x y;

Stdlib/Data/Range.juvix

@@ -30,7 +30,7 @@ for
       {-# specialize-by: [f] #-}
       terminating
       go (acc : A) (n : N) : A :=
-        if (n > high) acc (go (f acc n) (n + step));
+        ite (n > high) acc (go (f acc n) (n + step));
     in go a low;
 
 syntax operator to range;

Stdlib/Extra/Gcd.juvix

@@ -19,5 +19,5 @@ gcd
     -- Internal helper for computing the greatest common divisor. The first element
     -- should be smaller than the second.
     terminating
-    gcd' (a b : A) : A := if (a == 0) b (gcd' (mod b a) a);
-  in if (a > b) (gcd' b a) (gcd' a b);
+    gcd' (a b : A) : A := ite (a == 0) b (gcd' (mod b a) a);
+  in ite (a > b) (gcd' b a) (gcd' a b);

Stdlib/Trait/Ord.juvix

@@ -68,8 +68,8 @@ syntax operator >= comparison;
 
 --- Returns the smaller element.
 {-# inline: always #-}
-min {A} {{Ord A}} (x y : A) : A := if (x < y) x y;
+min {A} {{Ord A}} (x y : A) : A := ite (x < y) x y;
 
 --- Returns the larger element.
 {-# inline: always #-}
-max {A} {{Ord A}} (x y : A) : A := if (x > y) x y;
+max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y;