From 82e6b5f5d2fd478292f59d89937e422698976ab6 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 2 Jul 2024 10:03:06 +0200
Subject: [PATCH] Merge `if` -> `ite` renaming from stdlib (#2869)

---
 examples/demo/Demo.juvix                      |  2 +-
 examples/midsquare/MidSquareHash.juvix        |  2 +-
 .../midsquare/MidSquareHashUnrolled.juvix     | 26 +++++++++----------
 examples/milestone/Bank/Bank.juvix            |  6 ++---
 examples/milestone/Collatz/Collatz.juvix      |  2 +-
 examples/milestone/TicTacToe/Logic/Game.juvix |  8 +++---
 .../milestone/TicTacToe/Logic/Square.juvix    |  2 +-
 juvix-stdlib                                  |  2 +-
 .../Anoma/Compilation/positive/test006.juvix  |  2 +-
 .../Anoma/Compilation/positive/test012.juvix  |  4 +--
 .../Anoma/Compilation/positive/test013.juvix  |  6 ++---
 .../Anoma/Compilation/positive/test015.juvix  |  4 +--
 .../Anoma/Compilation/positive/test020.juvix  |  4 +--
 .../Anoma/Compilation/positive/test021.juvix  |  4 +--
 .../Anoma/Compilation/positive/test023.juvix  |  6 ++---
 .../Anoma/Compilation/positive/test024.juvix  |  2 +-
 .../Anoma/Compilation/positive/test025.juvix  |  2 +-
 .../Anoma/Compilation/positive/test028.juvix  |  2 +-
 .../Anoma/Compilation/positive/test032.juvix  |  6 ++---
 .../Anoma/Compilation/positive/test034.juvix  |  6 ++---
 .../Anoma/Compilation/positive/test060.juvix  |  2 +-
 .../Anoma/Compilation/positive/test064.juvix  |  6 ++---
 .../Anoma/Compilation/positive/test071.juvix  |  2 +-
 tests/Casm/Compilation/positive/test006.juvix |  8 +++---
 tests/Casm/Compilation/positive/test007.juvix |  4 +--
 tests/Casm/Compilation/positive/test013.juvix |  6 ++---
 tests/Casm/Compilation/positive/test015.juvix |  4 +--
 tests/Casm/Compilation/positive/test020.juvix |  4 +--
 tests/Casm/Compilation/positive/test021.juvix |  4 +--
 tests/Casm/Compilation/positive/test023.juvix |  6 ++---
 tests/Casm/Compilation/positive/test024.juvix |  2 +-
 tests/Casm/Compilation/positive/test025.juvix |  2 +-
 tests/Casm/Compilation/positive/test026.juvix |  2 +-
 tests/Casm/Compilation/positive/test028.juvix |  2 +-
 tests/Casm/Compilation/positive/test032.juvix |  6 ++---
 tests/Casm/Compilation/positive/test034.juvix |  6 ++---
 tests/Casm/Compilation/positive/test039.juvix |  2 +-
 tests/Casm/Compilation/positive/test040.juvix |  2 +-
 tests/Casm/Compilation/positive/test060.juvix |  2 +-
 tests/Casm/Compilation/positive/test064.juvix |  6 ++---
 tests/Casm/Compilation/positive/test069.juvix |  2 +-
 tests/Casm/Compilation/positive/test071.juvix |  2 +-
 tests/Casm/Compilation/positive/test077.juvix |  2 +-
 tests/Compilation/positive/test006.juvix      |  2 +-
 tests/Compilation/positive/test007.juvix      |  2 +-
 tests/Compilation/positive/test013.juvix      |  6 ++---
 tests/Compilation/positive/test015.juvix      |  2 +-
 tests/Compilation/positive/test020.juvix      |  4 +--
 tests/Compilation/positive/test023.juvix      |  6 ++---
 tests/Compilation/positive/test024.juvix      |  2 +-
 tests/Compilation/positive/test025.juvix      |  1 -
 tests/Compilation/positive/test026.juvix      |  2 +-
 tests/Compilation/positive/test028.juvix      |  2 +-
 tests/Compilation/positive/test032.juvix      |  4 +--
 tests/Compilation/positive/test034.juvix      |  6 ++---
 tests/Compilation/positive/test061.juvix      |  2 +-
 tests/Compilation/positive/test064.juvix      |  6 ++---
 tests/Compilation/positive/test071.juvix      |  2 +-
 tests/Geb/positive/Compilation/test001.juvix  |  2 +-
 tests/Geb/positive/Compilation/test002.juvix  |  2 +-
 tests/Geb/positive/Compilation/test003.juvix  |  2 +-
 tests/Geb/positive/Compilation/test008.juvix  |  2 +-
 tests/Geb/positive/Compilation/test010.juvix  |  6 ++---
 tests/Geb/positive/Compilation/test012.juvix  | 26 +++++++++----------
 tests/Geb/positive/Compilation/test016.juvix  |  4 +--
 tests/Geb/positive/Compilation/test020.juvix  |  2 +-
 tests/Geb/positive/Compilation/test021.juvix  |  4 +--
 tests/Geb/positive/Compilation/test022.juvix  |  6 ++---
 tests/Geb/positive/Compilation/test023.juvix  |  2 +-
 tests/Geb/positive/Compilation/test025.juvix  |  2 +-
 tests/Geb/positive/Compilation/test026.juvix  |  6 ++---
 tests/Internal/Core/positive/test006.juvix    |  2 +-
 tests/Internal/positive/BuiltinIf.juvix       |  2 +-
 tests/Internal/positive/QuickSort.juvix       |  2 +-
 tests/Rust/Compilation/positive/test006.juvix |  8 +++---
 tests/Rust/Compilation/positive/test007.juvix |  4 +--
 tests/Rust/Compilation/positive/test013.juvix |  6 ++---
 tests/Rust/Compilation/positive/test015.juvix |  4 +--
 tests/Rust/Compilation/positive/test020.juvix |  4 +--
 tests/Rust/Compilation/positive/test023.juvix |  6 ++---
 tests/Rust/Compilation/positive/test024.juvix |  2 +-
 tests/Rust/Compilation/positive/test025.juvix |  2 +-
 tests/Rust/Compilation/positive/test026.juvix |  2 +-
 tests/Rust/Compilation/positive/test028.juvix |  2 +-
 tests/Rust/Compilation/positive/test032.juvix |  6 ++---
 tests/Rust/Compilation/positive/test034.juvix |  6 ++---
 tests/Rust/Compilation/positive/test039.juvix |  2 +-
 tests/Rust/Compilation/positive/test040.juvix |  2 +-
 tests/Rust/Compilation/positive/test060.juvix |  2 +-
 tests/Rust/Compilation/positive/test064.juvix |  6 ++---
 tests/Rust/Compilation/positive/test069.juvix |  2 +-
 tests/Rust/Compilation/positive/test071.juvix |  2 +-
 .../VampIR/positive/Compilation/test001.juvix |  2 +-
 .../VampIR/positive/Compilation/test002.juvix |  6 ++---
 .../VampIR/positive/Compilation/test003.juvix |  6 ++---
 .../VampIR/positive/Compilation/test006.juvix |  6 ++---
 .../VampIR/positive/Compilation/test008.juvix |  6 ++---
 .../VampIR/positive/Compilation/test010.juvix | 26 +++++++++----------
 .../VampIR/positive/Compilation/test022.juvix |  4 +--
 .../VampIR/positive/Compilation/test023.juvix |  2 +-
 .../combinations/juvix/combinations.juvix     |  2 +-
 tests/benchmark/mapfold/juvix/mapfold.juvix   |  2 +-
 tests/benchmark/mapfun/juvix/mapfun.juvix     |  2 +-
 tests/benchmark/maybe/juvix/maybe.juvix       |  2 +-
 .../benchmark/mergesort/juvix/mergesort.juvix |  6 ++---
 tests/benchmark/prime/juvix/prime.juvix       |  6 ++---
 tests/negative/230/Foo/Data/Bool.juvix        |  2 +-
 tests/negative/Internal/LazyBuiltin.juvix     |  4 +--
 tests/positive/BuiltinsBool.juvix             |  2 +-
 tests/positive/Format.juvix                   |  4 +--
 tests/positive/Internal/Implicit.juvix        |  6 ++---
 tests/positive/Internal/Lambda.juvix          |  6 ++---
 tests/positive/issue1731/builtinTrace.juvix   |  2 +-
 113 files changed, 237 insertions(+), 238 deletions(-)

diff --git a/examples/demo/Demo.juvix b/examples/demo/Demo.juvix
index 11de93e94f..9c9c542e87 100644
--- a/examples/demo/Demo.juvix
+++ b/examples/demo/Demo.juvix
@@ -14,7 +14,7 @@ even' : Nat → Bool
 -- base 2 logarithm rounded down
 terminating
 log2 : Nat → Nat
-  | n := if (n <= 1) 0 (suc (log2 (div n 2)));
+  | n := ite (n <= 1) 0 (suc (log2 (div n 2)));
 
 type Tree (A : Type) :=
   | leaf : A → Tree A
diff --git a/examples/midsquare/MidSquareHash.juvix b/examples/midsquare/MidSquareHash.juvix
index cafd295dbe..731b548b97 100644
--- a/examples/midsquare/MidSquareHash.juvix
+++ b/examples/midsquare/MidSquareHash.juvix
@@ -15,7 +15,7 @@ pow : Nat -> Nat
 --- (i.e. smaller than 64) using the mid-square algorithm.
 hash' : Nat -> Nat -> Nat
   | (suc n@(suc (suc m))) x :=
-    if
+    ite
       (x < pow n)
       (hash' n x)
       (mod (div (x * x) (pow m)) (pow 6))
diff --git a/examples/midsquare/MidSquareHashUnrolled.juvix b/examples/midsquare/MidSquareHashUnrolled.juvix
index d9f0710300..80468695db 100644
--- a/examples/midsquare/MidSquareHashUnrolled.juvix
+++ b/examples/midsquare/MidSquareHashUnrolled.juvix
@@ -58,55 +58,55 @@ hash3 : Nat -> Nat
 
 hash4 : Nat -> Nat
   | x :=
-    if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+    ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
 hash5 : Nat -> Nat
   | x :=
-    if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+    ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
 hash6 : Nat -> Nat
   | x :=
-    if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+    ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
 hash7 : Nat -> Nat
   | x :=
-    if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+    ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
 hash8 : Nat -> Nat
   | x :=
-    if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+    ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
 hash9 : Nat -> Nat
   | x :=
-    if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+    ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
 hash10 : Nat -> Nat
   | x :=
-    if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+    ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
 hash11 : Nat -> Nat
   | x :=
-    if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+    ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
 hash12 : Nat -> Nat
   | x :=
-    if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+    ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
 hash13 : Nat -> Nat
   | x :=
-    if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+    ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
 hash14 : Nat -> Nat
   | x :=
-    if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+    ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
 hash15 : Nat -> Nat
   | x :=
-    if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+    ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
 hash16 : Nat -> Nat
   | x :=
-    if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+    ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 
diff --git a/examples/milestone/Bank/Bank.juvix b/examples/milestone/Bank/Bank.juvix
index 3781392529..01550e94cd 100644
--- a/examples/milestone/Bank/Bank.juvix
+++ b/examples/milestone/Bank/Bank.juvix
@@ -40,7 +40,7 @@ module Balances;
   increment : Field -> Nat -> Balances -> Balances
     | f n nil := (f, n) :: nil
     | f n ((b, bn) :: bs) :=
-      if
+      ite
         (f == b)
         ((b, bn + n) :: bs)
         ((b, bn) :: increment f n bs);
@@ -51,7 +51,7 @@ module Balances;
   decrement : Field -> Nat -> Balances -> Balances
     | _ _ nil := nil
     | f n ((b, bn) :: bs) :=
-      if
+      ite
         (f == b)
         ((b, sub bn n) :: bs)
         ((b, bn) :: decrement f n bs);
@@ -80,7 +80,7 @@ calculateInterest : Nat -> Nat -> Nat -> Nat
 
 --- Asserts some ;Bool; condition.
 assert : {A : Type} -> Bool -> A -> A
-  | c a := if c a (failwith "assertion failed");
+  | c a := ite c a (failwith "assertion failed");
 
 --- Returns a new ;Token;. Arguments are:
 ---
diff --git a/examples/milestone/Collatz/Collatz.juvix b/examples/milestone/Collatz/Collatz.juvix
index e697b1b5c2..71663a9d25 100644
--- a/examples/milestone/Collatz/Collatz.juvix
+++ b/examples/milestone/Collatz/Collatz.juvix
@@ -3,7 +3,7 @@ module Collatz;
 import Stdlib.Prelude open;
 
 collatzNext (n : Nat) : Nat :=
-  if (mod n 2 == 0) (div n 2) (3 * n + 1);
+  ite (mod n 2 == 0) (div n 2) (3 * n + 1);
 
 collatz : Nat → Nat
   | zero := zero
diff --git a/examples/milestone/TicTacToe/Logic/Game.juvix b/examples/milestone/TicTacToe/Logic/Game.juvix
index fc825929c9..37a454f7ef 100644
--- a/examples/milestone/TicTacToe/Logic/Game.juvix
+++ b/examples/milestone/TicTacToe/Logic/Game.juvix
@@ -12,14 +12,14 @@ import Logic.GameState open public;
 --- Checks if we reached the end of the game.
 checkState : GameState → GameState
   | (state b p e) :=
-    if
+    ite
       (won (state b p e))
       (state
         b
         p
         (terminate
           ("Player " ++str showSymbol (switch p) ++str " wins!")))
-      (if
+      (ite
         (draw (state b p e))
         (state b p (terminate "It's a draw!"))
         (state b p e));
@@ -29,7 +29,7 @@ playMove : Maybe Nat → GameState → GameState
   | nothing (state b p _) :=
     state b p (continue "\nInvalid number, try again\n")
   | (just k) (state (board s) player e) :=
-    if
+    ite
       (not (elem (==) k (possibleMoves (flatten s))))
       (state
         (board s)
@@ -43,4 +43,4 @@ playMove : Maybe Nat → GameState → GameState
 
 --- Returns ;just; if the given ;Nat; is in range of 1..9
 validMove (n : Nat) : Maybe Nat :=
-  if (n <= 9 && n >= 1) (just n) nothing;
+  ite (n <= 9 && n >= 1) (just n) nothing;
diff --git a/examples/milestone/TicTacToe/Logic/Square.juvix b/examples/milestone/TicTacToe/Logic/Square.juvix
index cb51144f57..b60017e5b6 100644
--- a/examples/milestone/TicTacToe/Logic/Square.juvix
+++ b/examples/milestone/TicTacToe/Logic/Square.juvix
@@ -23,5 +23,5 @@ showSquare : Square → String
   | (occupied s) := " " ++str showSymbol s ++str " ";
 
 replace (player : Symbol) (k : Nat) : Square → Square
-  | (empty n) := if (n == k) (occupied player) (empty n)
+  | (empty n) := ite (n == k) (occupied player) (empty n)
   | s := s;
diff --git a/juvix-stdlib b/juvix-stdlib
index 00f6f503db..50acdf1169 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit 00f6f503dbc2cfa72bd469fb8ce7edd0e9730639
+Subproject commit 50acdf11697d014fa9f02ce801cfbc31f6900003
diff --git a/tests/Anoma/Compilation/positive/test006.juvix b/tests/Anoma/Compilation/positive/test006.juvix
index 2d6d997321..6aab2363cb 100644
--- a/tests/Anoma/Compilation/positive/test006.juvix
+++ b/tests/Anoma/Compilation/positive/test006.juvix
@@ -9,6 +9,6 @@ loop : Nat := loop;
 
 main : Bool :=
   trace
-      (if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1))
+      (ite (3 > 0) 1 loop + ite (2 < 1) loop (ite (7 >= 8) loop 1))
     >-> trace (2 > 0 || loop == 0)
     >-> 2 < 0 && loop == 0;
diff --git a/tests/Anoma/Compilation/positive/test012.juvix b/tests/Anoma/Compilation/positive/test012.juvix
index 17818374ac..a8e55613ea 100644
--- a/tests/Anoma/Compilation/positive/test012.juvix
+++ b/tests/Anoma/Compilation/positive/test012.juvix
@@ -14,10 +14,10 @@ terminating
 gen : Nat → Tree
   | zero := leaf
   | n :=
-    if
+    ite
       (mod n 3 == 0)
       (node1 (gen (sub n 1)))
-      (if
+      (ite
         (mod n 3 == 1)
         (node2 (gen (sub n 1)) (gen (sub n 1)))
         (node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1))));
diff --git a/tests/Anoma/Compilation/positive/test013.juvix b/tests/Anoma/Compilation/positive/test013.juvix
index 9b0574404a..ba0fefb622 100644
--- a/tests/Anoma/Compilation/positive/test013.juvix
+++ b/tests/Anoma/Compilation/positive/test013.juvix
@@ -6,13 +6,13 @@ import Stdlib.Debug.Trace open;
 
 f : Nat → Nat → Nat
   | x :=
-    if
+    ite
       (x == 6)
       λ {_ := 0}
-      (if
+      (ite
         (x == 5)
         λ {_ := 1}
-        (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
+        (ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
 
 main : Nat :=
   trace (f 5 6)
diff --git a/tests/Anoma/Compilation/positive/test015.juvix b/tests/Anoma/Compilation/positive/test015.juvix
index eb93c97b6b..d1be20e13d 100644
--- a/tests/Anoma/Compilation/positive/test015.juvix
+++ b/tests/Anoma/Compilation/positive/test015.juvix
@@ -9,10 +9,10 @@ f : Nat → Nat → Nat
   | x :=
     let
       g (y : Nat) : Nat := x + y;
-    in if
+    in ite
       (x == 0)
       (f 10)
-      (if (x < 10) λ {y := g (f (sub x 1) y)} g);
+      (ite (x < 10) λ {y := g (f (sub x 1) y)} g);
 
 g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
 
diff --git a/tests/Anoma/Compilation/positive/test020.juvix b/tests/Anoma/Compilation/positive/test020.juvix
index 6f516f29cd..afc0d9748a 100644
--- a/tests/Anoma/Compilation/positive/test020.juvix
+++ b/tests/Anoma/Compilation/positive/test020.juvix
@@ -7,12 +7,12 @@ import Stdlib.Debug.Trace open;
 -- McCarthy's 91 function
 terminating
 f91 : Nat → Nat
-  | n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
+  | n := ite (n > 100) (sub n 10) (f91 (f91 (n + 11)));
 
 -- subtraction by increments
 terminating
 subp : Nat → Nat → Nat
-  | i j := if (i == j) 0 (subp i (j + 1) + 1);
+  | i j := ite (i == j) 0 (subp i (j + 1) + 1);
 
 main : Nat :=
   trace (f91 101)
diff --git a/tests/Anoma/Compilation/positive/test021.juvix b/tests/Anoma/Compilation/positive/test021.juvix
index 2130e3ef04..93681e1c3d 100644
--- a/tests/Anoma/Compilation/positive/test021.juvix
+++ b/tests/Anoma/Compilation/positive/test021.juvix
@@ -7,10 +7,10 @@ import Stdlib.Debug.Trace open;
 terminating
 power' : Nat → Nat → Nat → Nat
   | acc a b :=
-    if
+    ite
       (b == 0)
       acc
-      (if
+      (ite
         (mod b 2 == 0)
         (power' acc (a * a) (div b 2))
         (power' (acc * a) (a * a) (div b 2)));
diff --git a/tests/Anoma/Compilation/positive/test023.juvix b/tests/Anoma/Compilation/positive/test023.juvix
index 706408b22d..5ef3411487 100644
--- a/tests/Anoma/Compilation/positive/test023.juvix
+++ b/tests/Anoma/Compilation/positive/test023.juvix
@@ -7,14 +7,14 @@ import Stdlib.Debug.Trace open;
 terminating
 f : Nat → Nat
 
-  | x := if (x < 1) 1 (2 * x + g (sub x 1));
+  | x := ite (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
 g : Nat → Nat
-  | x := if (x < 1) 1 (x + h (sub x 1));
+  | x := ite (x < 1) 1 (x + h (sub x 1));
 
 terminating
 h : Nat → Nat
-  | x := if (x < 1) 1 (x * f (sub x 1));
+  | x := ite (x < 1) 1 (x * f (sub x 1));
 
 main : Nat := trace (f 5) >-> trace (f 10) >-> f 20;
diff --git a/tests/Anoma/Compilation/positive/test024.juvix b/tests/Anoma/Compilation/positive/test024.juvix
index 93e342f2ef..2f152826b0 100644
--- a/tests/Anoma/Compilation/positive/test024.juvix
+++ b/tests/Anoma/Compilation/positive/test024.juvix
@@ -15,7 +15,7 @@ gen : Nat → Tree
 g : Tree → Tree
 
   | leaf := leaf
-  | (node l r) := if (isNode l) r (node r l);
+  | (node l r) := ite (isNode l) r (node r l);
 
 terminating
 f : Tree → Nat
diff --git a/tests/Anoma/Compilation/positive/test025.juvix b/tests/Anoma/Compilation/positive/test025.juvix
index bd2b1cfef9..f7f06882d5 100644
--- a/tests/Anoma/Compilation/positive/test025.juvix
+++ b/tests/Anoma/Compilation/positive/test025.juvix
@@ -7,7 +7,7 @@ import Stdlib.Debug.Trace open;
 terminating
 gcd : Nat → Nat → Nat
   | a b :=
-    if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
+    ite (a > b) (gcd b a) (ite (a == 0) b (gcd (mod b a) a));
 
 main : Nat :=
   trace (gcd (3 * 7 * 2) (7 * 2 * 11))
diff --git a/tests/Anoma/Compilation/positive/test028.juvix b/tests/Anoma/Compilation/positive/test028.juvix
index e5b34db0c6..14a4d40d06 100644
--- a/tests/Anoma/Compilation/positive/test028.juvix
+++ b/tests/Anoma/Compilation/positive/test028.juvix
@@ -15,7 +15,7 @@ sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
   | p s unit :=
     case force s of
       cons h t :=
-        if (p h) (cons h (sfilter p t)) (force (sfilter p t));
+        ite (p h) (cons h (sfilter p t)) (force (sfilter p t));
 
 shead : Stream → Nat
   | (cons h _) := h;
diff --git a/tests/Anoma/Compilation/positive/test032.juvix b/tests/Anoma/Compilation/positive/test032.juvix
index 732989dfe5..9e7c46a2e7 100644
--- a/tests/Anoma/Compilation/positive/test032.juvix
+++ b/tests/Anoma/Compilation/positive/test032.juvix
@@ -15,14 +15,14 @@ merge' : List Nat → List Nat → List Nat
   | nil ys := ys
   | xs nil := xs
   | xs@(x :: xs') ys@(y :: ys') :=
-    if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
+    ite (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
 
 terminating
 sort : List Nat → List Nat
   | xs :=
     let
       n : Nat := length xs;
-    in if
+    in ite
       (n <= 1)
       xs
       case split (div n 2) xs of {l1, l2 :=
@@ -33,7 +33,7 @@ uniq : List Nat → List Nat
   | nil := nil
   | (x :: nil) := x :: nil
   | (x :: xs@(x' :: _)) :=
-    if (x == x') (uniq xs) (x :: uniq xs);
+    ite (x == x') (uniq xs) (x :: uniq xs);
 
 gen : List Nat → Nat → (Nat → Nat) → List Nat
   | acc zero f := acc
diff --git a/tests/Anoma/Compilation/positive/test034.juvix b/tests/Anoma/Compilation/positive/test034.juvix
index 99ac0798bf..fe3c518e7f 100644
--- a/tests/Anoma/Compilation/positive/test034.juvix
+++ b/tests/Anoma/Compilation/positive/test034.juvix
@@ -16,11 +16,11 @@ sum : Nat → Nat :=
 mutrec : Nat :=
   let
     terminating
-    f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
+    f (x : Nat) : Nat := ite (x < 1) 1 (g (sub x 1) + 2 * x);
     terminating
-    g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
+    g (x : Nat) : Nat := ite (x < 1) 1 (x + h (sub x 1));
     terminating
-    h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
+    h (x : Nat) : Nat := ite (x < 1) 1 (x * f (sub x 1));
   in trace (f 5)
     >-> trace (f 10)
     >-> trace (g 5)
diff --git a/tests/Anoma/Compilation/positive/test060.juvix b/tests/Anoma/Compilation/positive/test060.juvix
index abc4643161..67992e75ff 100644
--- a/tests/Anoma/Compilation/positive/test060.juvix
+++ b/tests/Anoma/Compilation/positive/test060.juvix
@@ -31,7 +31,7 @@ main : Triple Nat Nat Nat :=
       };
     f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
       (@Triple{fst := fst * 10});
-  in if
+  in ite
     (mf
       mkPair@{
         fst := mkPair true nil;
diff --git a/tests/Anoma/Compilation/positive/test064.juvix b/tests/Anoma/Compilation/positive/test064.juvix
index e52005dc82..c2a91b8eeb 100644
--- a/tests/Anoma/Compilation/positive/test064.juvix
+++ b/tests/Anoma/Compilation/positive/test064.juvix
@@ -9,10 +9,10 @@ f (x y : Nat) : Nat := x + y;
 
 -- TODO: Replace loop with failwith when anoma backend supports strings
 {-# inline: false #-}
-g (x : Bool) : Bool := if x loop true;
+g (x : Bool) : Bool := ite x loop true;
 
 {-# inline: false #-}
-h (x : Bool) : Bool := if (g x) false true;
+h (x : Bool) : Bool := ite (g x) false true;
 
 {-# inline: false, eval: false #-}
 j (x : Nat) : Nat := x + 0;
@@ -38,6 +38,6 @@ even' : Nat -> Bool := even;
 main : Nat :=
   sum 3
     + case even' 6 || g true || h true of {
-        | true := if (g false) (f 1 2 + sum 7 + j 0) 0
+        | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
         | false := f (3 + 4) (f 0 8) + loop
       };
diff --git a/tests/Anoma/Compilation/positive/test071.juvix b/tests/Anoma/Compilation/positive/test071.juvix
index d552c66825..f5bd48deb0 100644
--- a/tests/Anoma/Compilation/positive/test071.juvix
+++ b/tests/Anoma/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 +
+  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
   h@?{b := 4} 1;
diff --git a/tests/Casm/Compilation/positive/test006.juvix b/tests/Casm/Compilation/positive/test006.juvix
index 2032d091a4..bc285cf1af 100644
--- a/tests/Casm/Compilation/positive/test006.juvix
+++ b/tests/Casm/Compilation/positive/test006.juvix
@@ -7,7 +7,7 @@ terminating
 loop : Nat := loop;
 
 main : Nat :=
-  if (3 > 0) 1 loop
-    + if (2 < 1) loop (if (7 >= 8) loop 1)
-    + if (2 > 0 || loop == 0) 1 0
-    + if (2 < 0 && loop == 0) 1 0;
+  ite (3 > 0) 1 loop
+    + ite (2 < 1) loop (ite (7 >= 8) loop 1)
+    + ite (2 > 0 || loop == 0) 1 0
+    + ite (2 < 0 && loop == 0) 1 0;
diff --git a/tests/Casm/Compilation/positive/test007.juvix b/tests/Casm/Compilation/positive/test007.juvix
index 998b804c07..b2c114dec7 100644
--- a/tests/Casm/Compilation/positive/test007.juvix
+++ b/tests/Casm/Compilation/positive/test007.juvix
@@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
 lst : List Nat := 0 :: 1 :: nil;
 
 main : Nat :=
-  if (null lst) 1 0
-    + if (null (nil {Nat})) 1 0
+  ite (null lst) 1 0
+    + ite (null (nil {Nat})) 1 0
     + head 1 lst
     + head 0 (tail lst)
     + head 0 (tail (map ((+) 1) lst))
diff --git a/tests/Casm/Compilation/positive/test013.juvix b/tests/Casm/Compilation/positive/test013.juvix
index b0d63c9a81..52544cb108 100644
--- a/tests/Casm/Compilation/positive/test013.juvix
+++ b/tests/Casm/Compilation/positive/test013.juvix
@@ -5,12 +5,12 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | x :=
-    if
+    ite
       (x == 6)
       λ {_ := 0}
-      (if
+      (ite
         (x == 5)
         λ {_ := 1}
-        (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
+        (ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
 
 main : Nat := f 5 6 + f 6 5 + f 10 5 + f 11 5;
diff --git a/tests/Casm/Compilation/positive/test015.juvix b/tests/Casm/Compilation/positive/test015.juvix
index 6c6486d628..43b5edea02 100644
--- a/tests/Casm/Compilation/positive/test015.juvix
+++ b/tests/Casm/Compilation/positive/test015.juvix
@@ -8,10 +8,10 @@ f : Nat → Nat → Nat
   | x :=
     let
       g (y : Nat) : Nat := x + y;
-    in if
+    in ite
       (x == 0)
       (f 10)
-      (if (x < 10) λ {y := g (f (sub x 1) y)} g);
+      (ite (x < 10) λ {y := g (f (sub x 1) y)} g);
 
 g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
 
diff --git a/tests/Casm/Compilation/positive/test020.juvix b/tests/Casm/Compilation/positive/test020.juvix
index 4cd552d220..64f6743095 100644
--- a/tests/Casm/Compilation/positive/test020.juvix
+++ b/tests/Casm/Compilation/positive/test020.juvix
@@ -6,12 +6,12 @@ import Stdlib.Prelude open;
 -- McCarthy's 91 function
 terminating
 f91 : Nat → Nat
-  | n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
+  | n := ite (n > 100) (sub n 10) (f91 (f91 (n + 11)));
 
 -- subtraction by increments
 terminating
 subp : Nat → Nat → Nat
-  | i j := if (i == j) 0 (subp i (j + 1) + 1);
+  | i j := ite (i == j) 0 (subp i (j + 1) + 1);
 
 main : Nat :=
   f91 101
diff --git a/tests/Casm/Compilation/positive/test021.juvix b/tests/Casm/Compilation/positive/test021.juvix
index 63ebdbaf39..14adf2a5f0 100644
--- a/tests/Casm/Compilation/positive/test021.juvix
+++ b/tests/Casm/Compilation/positive/test021.juvix
@@ -6,10 +6,10 @@ import Stdlib.Prelude open;
 terminating
 power' : Nat → Nat → Nat → Nat
   | acc a b :=
-    if
+    ite
       (b == 0)
       acc
-      (if
+      (ite
         (mod b 2 == 0)
         (power' acc (a * a) (div b 2))
         (power' (acc * a) (a * a) (div b 2)));
diff --git a/tests/Casm/Compilation/positive/test023.juvix b/tests/Casm/Compilation/positive/test023.juvix
index 26cb5429ab..0414f08853 100644
--- a/tests/Casm/Compilation/positive/test023.juvix
+++ b/tests/Casm/Compilation/positive/test023.juvix
@@ -6,14 +6,14 @@ import Stdlib.Prelude open;
 terminating
 f : Nat → Nat
 
-  | x := if (x < 1) 1 (2 * x + g (sub x 1));
+  | x := ite (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
 g : Nat → Nat
-  | x := if (x < 1) 1 (x + h (sub x 1));
+  | x := ite (x < 1) 1 (x + h (sub x 1));
 
 terminating
 h : Nat → Nat
-  | x := if (x < 1) 1 (x * f (sub x 1));
+  | x := ite (x < 1) 1 (x * f (sub x 1));
 
 main : Nat := f 5 + f 10 + f 20;
diff --git a/tests/Casm/Compilation/positive/test024.juvix b/tests/Casm/Compilation/positive/test024.juvix
index 83d3acdda3..b5b5aaa213 100644
--- a/tests/Casm/Compilation/positive/test024.juvix
+++ b/tests/Casm/Compilation/positive/test024.juvix
@@ -15,7 +15,7 @@ gen : Nat → Tree
 g : Tree → Tree
 
   | leaf := leaf
-  | (node l r) := if (isNode l) r (node r l);
+  | (node l r) := ite (isNode l) r (node r l);
 
 terminating
 f : Tree → Nat
diff --git a/tests/Casm/Compilation/positive/test025.juvix b/tests/Casm/Compilation/positive/test025.juvix
index ceb84cd312..1e1d35ef3d 100644
--- a/tests/Casm/Compilation/positive/test025.juvix
+++ b/tests/Casm/Compilation/positive/test025.juvix
@@ -6,7 +6,7 @@ import Stdlib.Prelude open;
 terminating
 gcd : Nat → Nat → Nat
   | a b :=
-    if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
+    ite (a > b) (gcd b a) (ite (a == 0) b (gcd (mod b a) a));
 
 main : Nat :=
   gcd (3 * 7 * 2) (7 * 2 * 11)
diff --git a/tests/Casm/Compilation/positive/test026.juvix b/tests/Casm/Compilation/positive/test026.juvix
index f3cc2b1a6c..e91eafc367 100644
--- a/tests/Casm/Compilation/positive/test026.juvix
+++ b/tests/Casm/Compilation/positive/test026.juvix
@@ -43,7 +43,7 @@ empty : {A : Type} → Queue A := queue nil nil;
 terminating
 g {{Partial}} : List Nat → Queue Nat → List Nat
   | acc q :=
-    if (is_empty q) acc (g (front q :: acc) (pop_front q));
+    ite (is_empty q) acc (g (front q :: acc) (pop_front q));
 
 f {{Partial}} : Nat → Queue Nat → List Nat
   | zero q := g nil q
diff --git a/tests/Casm/Compilation/positive/test028.juvix b/tests/Casm/Compilation/positive/test028.juvix
index c014a3a584..26a73be327 100644
--- a/tests/Casm/Compilation/positive/test028.juvix
+++ b/tests/Casm/Compilation/positive/test028.juvix
@@ -12,7 +12,7 @@ terminating
 sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
   | p s unit :=
     case force s of {cons h t :=
-      if (p h) (cons h (sfilter p t)) (force (sfilter p t))};
+      ite (p h) (cons h (sfilter p t)) (force (sfilter p t))};
 
 shead : Stream → Nat
   | (cons h _) := h;
diff --git a/tests/Casm/Compilation/positive/test032.juvix b/tests/Casm/Compilation/positive/test032.juvix
index b6932d7ac9..f720d33828 100644
--- a/tests/Casm/Compilation/positive/test032.juvix
+++ b/tests/Casm/Compilation/positive/test032.juvix
@@ -14,14 +14,14 @@ merge' : List Nat → List Nat → List Nat
   | nil ys := ys
   | xs nil := xs
   | xs@(x :: xs') ys@(y :: ys') :=
-    if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
+    ite (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
 
 terminating
 sort : List Nat → List Nat
   | xs :=
     let
       n : Nat := length xs;
-    in if
+    in ite
       (n <= 1)
       xs
       case split (div n 2) xs of {l1, l2 :=
@@ -32,7 +32,7 @@ uniq : List Nat → List Nat
   | nil := nil
   | (x :: nil) := x :: nil
   | (x :: xs@(x' :: _)) :=
-    if (x == x') (uniq xs) (x :: uniq xs);
+    ite (x == x') (uniq xs) (x :: uniq xs);
 
 gen : List Nat → Nat → (Nat → Nat) → List Nat
   | acc zero f := acc
diff --git a/tests/Casm/Compilation/positive/test034.juvix b/tests/Casm/Compilation/positive/test034.juvix
index 7176d15b5c..1877f8c77e 100644
--- a/tests/Casm/Compilation/positive/test034.juvix
+++ b/tests/Casm/Compilation/positive/test034.juvix
@@ -15,11 +15,11 @@ sum : Nat → Nat :=
 mutrec : Nat :=
   let
     terminating
-    f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
+    f (x : Nat) : Nat := ite (x < 1) 1 (g (sub x 1) + 2 * x);
     terminating
-    g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
+    g (x : Nat) : Nat := ite (x < 1) 1 (x + h (sub x 1));
     terminating
-    h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
+    h (x : Nat) : Nat := ite (x < 1) 1 (x * f (sub x 1));
   in f 5 + f 10 + g 5 + h 5;
 
 main : Nat := sum 10000 + mutrec;
diff --git a/tests/Casm/Compilation/positive/test039.juvix b/tests/Casm/Compilation/positive/test039.juvix
index 76d471bd28..c33d12f0cf 100644
--- a/tests/Casm/Compilation/positive/test039.juvix
+++ b/tests/Casm/Compilation/positive/test039.juvix
@@ -14,4 +14,4 @@ main : Nat :=
       | zero := true
       | (suc n) := not (odd n);
     plusOne (n : Ty) : Ty := n + 1;
-  in if (odd (plusOne 13)) 1 0 + if (even (plusOne 12)) 1 0;
+  in ite (odd (plusOne 13)) 1 0 + ite (even (plusOne 12)) 1 0;
diff --git a/tests/Casm/Compilation/positive/test040.juvix b/tests/Casm/Compilation/positive/test040.juvix
index 2d5fb89f25..039eac69c6 100644
--- a/tests/Casm/Compilation/positive/test040.juvix
+++ b/tests/Casm/Compilation/positive/test040.juvix
@@ -14,4 +14,4 @@ type Foo (A : Type) :=
 f : {A : Type} -> Foo A -> A
   | (foo unit a) := a;
 
-main : Nat := if (f (foo unit true)) 1 0;
+main : Nat := ite (f (foo unit true)) 1 0;
diff --git a/tests/Casm/Compilation/positive/test060.juvix b/tests/Casm/Compilation/positive/test060.juvix
index 7e352001f2..a7865ffaf0 100644
--- a/tests/Casm/Compilation/positive/test060.juvix
+++ b/tests/Casm/Compilation/positive/test060.juvix
@@ -34,7 +34,7 @@ main : Nat :=
       };
     f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
       (@Triple{fst := fst * 10});
-  in sum <| if
+  in sum <| ite
     (mf
       mkPair@{
         fst := mkPair true nil;
diff --git a/tests/Casm/Compilation/positive/test064.juvix b/tests/Casm/Compilation/positive/test064.juvix
index c3674c2730..17915e9e48 100644
--- a/tests/Casm/Compilation/positive/test064.juvix
+++ b/tests/Casm/Compilation/positive/test064.juvix
@@ -8,10 +8,10 @@ import Stdlib.Debug.Fail as Debug;
 f (x y : Nat) : Nat := x + y;
 
 {-# inline: false #-}
-g (x : Bool) : Bool := if x false true;
+g (x : Bool) : Bool := ite x false true;
 
 {-# inline: false #-}
-h (x : Bool) : Bool := if (g x) false true;
+h (x : Bool) : Bool := ite (g x) false true;
 
 {-# inline: false, eval: false #-}
 j (x : Nat) : Nat := x + 0;
@@ -37,6 +37,6 @@ even' : Nat -> Bool := even;
 main : Nat :=
   sum 3
     + case even' 6 || g true || h true of {
-        | true := if (g false) (f 1 2 + sum 7 + j 0) 0
+        | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
         | false := f (3 + 4) (f 0 8) + loop
       };
diff --git a/tests/Casm/Compilation/positive/test069.juvix b/tests/Casm/Compilation/positive/test069.juvix
index 0484d600d8..e5ec4e3f72 100644
--- a/tests/Casm/Compilation/positive/test069.juvix
+++ b/tests/Casm/Compilation/positive/test069.juvix
@@ -28,4 +28,4 @@ ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare);
 instance
 ordNat : Ord Nat := mkOrdHelper Ord.compare;
 
-main : Nat := if (Ord.lt 1 2) 1 0;
+main : Nat := ite (Ord.lt 1 2) 1 0;
diff --git a/tests/Casm/Compilation/positive/test071.juvix b/tests/Casm/Compilation/positive/test071.juvix
index d552c66825..f5bd48deb0 100644
--- a/tests/Casm/Compilation/positive/test071.juvix
+++ b/tests/Casm/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 +
+  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
   h@?{b := 4} 1;
diff --git a/tests/Casm/Compilation/positive/test077.juvix b/tests/Casm/Compilation/positive/test077.juvix
index 0e29998d92..f18da3a313 100644
--- a/tests/Casm/Compilation/positive/test077.juvix
+++ b/tests/Casm/Compilation/positive/test077.juvix
@@ -25,7 +25,7 @@ type ComplianceResult :=
 
 count : List (Pair Field Bool) -> Field
   | [] := 0
-  | ((h, b) :: t) := if b (h + count t) (count t);
+  | ((h, b) :: t) := ite b (h + count t) (count t);
 
 main
   (input : Resource)
diff --git a/tests/Compilation/positive/test006.juvix b/tests/Compilation/positive/test006.juvix
index 1e81893a29..4d8ae8376f 100644
--- a/tests/Compilation/positive/test006.juvix
+++ b/tests/Compilation/positive/test006.juvix
@@ -8,6 +8,6 @@ loop : Nat := loop;
 
 main : IO :=
   printNatLn
-      (if (3 > 0) 1 loop + if (2 < 1) loop (if (7 >= 8) loop 1))
+      (ite (3 > 0) 1 loop + ite (2 < 1) loop (ite (7 >= 8) loop 1))
     >>> printBoolLn (2 > 0 || loop == 0)
     >>> printBoolLn (2 < 0 && loop == 0);
diff --git a/tests/Compilation/positive/test007.juvix b/tests/Compilation/positive/test007.juvix
index 2f222eb073..300836c2fa 100644
--- a/tests/Compilation/positive/test007.juvix
+++ b/tests/Compilation/positive/test007.juvix
@@ -11,7 +11,7 @@ map' {A B} (f : A → B) : List A → List B :=
 
 terminating
 map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
-  if (null x) nil (f (phead x) :: map'' f (tail x));
+  ite (null x) nil (f (phead x) :: map'' f (tail x));
 
 lst : List Nat := 0 :: 1 :: nil;
 
diff --git a/tests/Compilation/positive/test013.juvix b/tests/Compilation/positive/test013.juvix
index 5c3f7fe737..0222fd3cea 100644
--- a/tests/Compilation/positive/test013.juvix
+++ b/tests/Compilation/positive/test013.juvix
@@ -5,13 +5,13 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | x :=
-    if
+    ite
       (x == 6)
       λ {_ := 0}
-      (if
+      (ite
         (x == 5)
         λ {_ := 1}
-        (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
+        (ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
 
 main : IO :=
   printNatLn (f 5 6)
diff --git a/tests/Compilation/positive/test015.juvix b/tests/Compilation/positive/test015.juvix
index adac4cdc93..de034271c4 100644
--- a/tests/Compilation/positive/test015.juvix
+++ b/tests/Compilation/positive/test015.juvix
@@ -10,7 +10,7 @@ f : Nat → Nat → Nat
       g (y : Nat) : Nat := x + y;
     in if
       | x == 0 := f 10
-      | else := if (x < 10) λ {y := g (f (sub x 1) y)} g;
+      | else := ite (x < 10) λ {y := g (f (sub x 1) y)} g;
 
 g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
 
diff --git a/tests/Compilation/positive/test020.juvix b/tests/Compilation/positive/test020.juvix
index 32243daca0..52190bea03 100644
--- a/tests/Compilation/positive/test020.juvix
+++ b/tests/Compilation/positive/test020.juvix
@@ -6,12 +6,12 @@ import Stdlib.Prelude open;
 -- McCarthy's 91 function
 terminating
 f91 : Nat → Nat
-  | n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
+  | n := ite (n > 100) (sub n 10) (f91 (f91 (n + 11)));
 
 -- subtraction by increments
 terminating
 subp : Nat → Nat → Nat
-  | i j := if (i == j) 0 (subp i (j + 1) + 1);
+  | i j := ite (i == j) 0 (subp i (j + 1) + 1);
 
 main : IO :=
   printNatLn (f91 101)
diff --git a/tests/Compilation/positive/test023.juvix b/tests/Compilation/positive/test023.juvix
index 2a0946bfe7..c740ff35a3 100644
--- a/tests/Compilation/positive/test023.juvix
+++ b/tests/Compilation/positive/test023.juvix
@@ -6,15 +6,15 @@ import Stdlib.Prelude open;
 terminating
 f : Nat → Nat
 
-  | x := if (x < 1) 1 (2 * x + g (sub x 1));
+  | x := ite (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
 g : Nat → Nat
-  | x := if (x < 1) 1 (x + h (sub x 1));
+  | x := ite (x < 1) 1 (x + h (sub x 1));
 
 terminating
 h : Nat → Nat
-  | x := if (x < 1) 1 (x * f (sub x 1));
+  | x := ite (x < 1) 1 (x * f (sub x 1));
 
 main : IO :=
   printNatLn (f 5)
diff --git a/tests/Compilation/positive/test024.juvix b/tests/Compilation/positive/test024.juvix
index 6c9535156e..ab8a5cb287 100644
--- a/tests/Compilation/positive/test024.juvix
+++ b/tests/Compilation/positive/test024.juvix
@@ -14,7 +14,7 @@ gen : Nat → Tree
 
 g : Tree → Tree
   | leaf := leaf
-  | (node l r) := if (isNode l) r (node r l);
+  | (node l r) := ite (isNode l) r (node r l);
 
 terminating
 f : Tree → Nat
diff --git a/tests/Compilation/positive/test025.juvix b/tests/Compilation/positive/test025.juvix
index 0176bc8609..23c494e400 100644
--- a/tests/Compilation/positive/test025.juvix
+++ b/tests/Compilation/positive/test025.juvix
@@ -17,4 +17,3 @@ main : IO :=
     >>> printNatLn (gcd 3 7)
     >>> printNatLn (gcd 7 3)
     >>> printNatLn (gcd (11 * 7 * 3) (2 * 5 * 13));
-
diff --git a/tests/Compilation/positive/test026.juvix b/tests/Compilation/positive/test026.juvix
index 6b254281db..b1896a46b0 100644
--- a/tests/Compilation/positive/test026.juvix
+++ b/tests/Compilation/positive/test026.juvix
@@ -43,7 +43,7 @@ empty : {A : Type} → Queue A := queue nil nil;
 terminating
 g {{Partial}} : List Nat → Queue Nat → List Nat
   | acc q :=
-    if (is_empty q) acc (g (front q :: acc) (pop_front q));
+    ite (is_empty q) acc (g (front q :: acc) (pop_front q));
 
 f {{Partial}} : Nat → Queue Nat → List Nat
   | zero q := g nil q
diff --git a/tests/Compilation/positive/test028.juvix b/tests/Compilation/positive/test028.juvix
index 64adbfcff1..7da7c11256 100644
--- a/tests/Compilation/positive/test028.juvix
+++ b/tests/Compilation/positive/test028.juvix
@@ -13,7 +13,7 @@ sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
   | p s unit :=
     case force s of
       cons h t :=
-        if (p h) (cons h (sfilter p t)) (force (sfilter p t));
+        ite (p h) (cons h (sfilter p t)) (force (sfilter p t));
 
 shead : Stream → Nat
   | (cons h _) := h;
diff --git a/tests/Compilation/positive/test032.juvix b/tests/Compilation/positive/test032.juvix
index 155be32116..ba99632e9d 100644
--- a/tests/Compilation/positive/test032.juvix
+++ b/tests/Compilation/positive/test032.juvix
@@ -14,7 +14,7 @@ merge' : List Nat → List Nat → List Nat
   | nil ys := ys
   | xs nil := xs
   | xs@(x :: xs') ys@(y :: ys') :=
-    if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
+    ite (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
 
 terminating
 sort : List Nat → List Nat
@@ -32,7 +32,7 @@ uniq : List Nat → List Nat
   | nil := nil
   | (x :: nil) := x :: nil
   | (x :: xs@(x' :: _)) :=
-    if (x == x') (uniq xs) (x :: uniq xs);
+    ite (x == x') (uniq xs) (x :: uniq xs);
 
 gen : List Nat → Nat → (Nat → Nat) → List Nat
   | acc zero f := acc
diff --git a/tests/Compilation/positive/test034.juvix b/tests/Compilation/positive/test034.juvix
index c5fe93a86d..e529cc5f7b 100644
--- a/tests/Compilation/positive/test034.juvix
+++ b/tests/Compilation/positive/test034.juvix
@@ -15,11 +15,11 @@ sum : Nat → Nat :=
 mutrec : IO :=
   let
     terminating
-    f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
+    f (x : Nat) : Nat := ite (x < 1) 1 (g (sub x 1) + 2 * x);
     terminating
-    g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
+    g (x : Nat) : Nat := ite (x < 1) 1 (x + h (sub x 1));
     terminating
-    h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
+    h (x : Nat) : Nat := ite (x < 1) 1 (x * f (sub x 1));
   in printNatLn (f 5)
     >>> printNatLn (f 10)
     >>> printNatLn (g 5)
diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix
index 089fe32edb..999b67bf73 100644
--- a/tests/Compilation/positive/test061.juvix
+++ b/tests/Compilation/positive/test061.juvix
@@ -15,7 +15,7 @@ showStringI : Show String := mkShow (show := id);
 instance
 showBoolI : Show' Bool' :=
   mkShow@{
-    show (x : Bool) : String := if x "true" "false"
+    show (x : Bool) : String := ite x "true" "false"
   };
 
 instance
diff --git a/tests/Compilation/positive/test064.juvix b/tests/Compilation/positive/test064.juvix
index e9fdb8e216..84c964c5a9 100644
--- a/tests/Compilation/positive/test064.juvix
+++ b/tests/Compilation/positive/test064.juvix
@@ -8,10 +8,10 @@ import Stdlib.Debug.Fail as Debug;
 f (x y : Nat) : Nat := x + y;
 
 {-# inline: false #-}
-g (x : Bool) : Bool := if x (Debug.failwith "a") true;
+g (x : Bool) : Bool := ite x (Debug.failwith "a") true;
 
 {-# inline: false #-}
-h (x : Bool) : Bool := if (g x) false true;
+h (x : Bool) : Bool := ite (g x) false true;
 
 {-# inline: false, eval: false #-}
 j (x : Nat) : Nat := x + 0;
@@ -37,5 +37,5 @@ even' : Nat -> Bool := even;
 main : Nat :=
   sum 3
     + case even' 6 || g true || h true of
-        | true := if (g false) (f 1 2 + sum 7 + j 0) 0
+        | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
         | false := f (3 + 4) (f 0 8) + loop;
diff --git a/tests/Compilation/positive/test071.juvix b/tests/Compilation/positive/test071.juvix
index d552c66825..f5bd48deb0 100644
--- a/tests/Compilation/positive/test071.juvix
+++ b/tests/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 +
+  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
   h@?{b := 4} 1;
diff --git a/tests/Geb/positive/Compilation/test001.juvix b/tests/Geb/positive/Compilation/test001.juvix
index de66290299..3a678ebab5 100644
--- a/tests/Geb/positive/Compilation/test001.juvix
+++ b/tests/Geb/positive/Compilation/test001.juvix
@@ -3,4 +3,4 @@ module test001;
 
 import Stdlib.Prelude open;
 
-main : Bool := λ {x := if x false true} true;
+main : Bool := λ {x := ite x false true} true;
diff --git a/tests/Geb/positive/Compilation/test002.juvix b/tests/Geb/positive/Compilation/test002.juvix
index 1d46ad9586..9369736025 100644
--- a/tests/Geb/positive/Compilation/test002.juvix
+++ b/tests/Geb/positive/Compilation/test002.juvix
@@ -9,7 +9,7 @@ type optbool :=
 
 main : Bool :=
   λ {
-      x (Just b) := if x true b
+      x (Just b) := ite x true b
       | _ Nothing := false
     }
     false
diff --git a/tests/Geb/positive/Compilation/test003.juvix b/tests/Geb/positive/Compilation/test003.juvix
index 7fe822a886..b0b94022a5 100644
--- a/tests/Geb/positive/Compilation/test003.juvix
+++ b/tests/Geb/positive/Compilation/test003.juvix
@@ -12,6 +12,6 @@ main : Bool :=
   λ {
       | opt0 := false
       | (opt1 b) := b
-      | (opt2 b c) := if b b c
+      | (opt2 b c) := ite b b c
     }
     (opt2 false true);
diff --git a/tests/Geb/positive/Compilation/test008.juvix b/tests/Geb/positive/Compilation/test008.juvix
index f2a94be4cd..46db5235aa 100644
--- a/tests/Geb/positive/Compilation/test008.juvix
+++ b/tests/Geb/positive/Compilation/test008.juvix
@@ -10,7 +10,7 @@ type enum :=
   | opt3 : Bool -> (Bool -> Bool -> Bool) -> Bool -> enum;
 
 main : Bool :=
-  case opt3 true λ {x y := if y false x} false of
+  case opt3 true λ {x y := ite y false x} false of
     | opt0 := false
     | opt1 b := b
     | opt2 b f := f b
diff --git a/tests/Geb/positive/Compilation/test010.juvix b/tests/Geb/positive/Compilation/test010.juvix
index 7db0cb4278..15e371ef0e 100644
--- a/tests/Geb/positive/Compilation/test010.juvix
+++ b/tests/Geb/positive/Compilation/test010.juvix
@@ -5,12 +5,12 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | x :=
-    if
+    ite
       (x == 6)
       λ {_ := 0}
-      (if
+      (ite
         (x == 5)
         λ {_ := 1}
-        (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
+        (ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
 
 main : Nat := f 5 6 + f 6 5 + f 10 5 + f 11 5;
diff --git a/tests/Geb/positive/Compilation/test012.juvix b/tests/Geb/positive/Compilation/test012.juvix
index 0c6b89a08b..6aac434459 100644
--- a/tests/Geb/positive/Compilation/test012.juvix
+++ b/tests/Geb/positive/Compilation/test012.juvix
@@ -51,55 +51,55 @@ hash3 : Nat -> Nat
 
 hash4 : Nat -> Nat
   | x :=
-    if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+    ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
 hash5 : Nat -> Nat
   | x :=
-    if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+    ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
 hash6 : Nat -> Nat
   | x :=
-    if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+    ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
 hash7 : Nat -> Nat
   | x :=
-    if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+    ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
 hash8 : Nat -> Nat
   | x :=
-    if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+    ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
 hash9 : Nat -> Nat
   | x :=
-    if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+    ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
 hash10 : Nat -> Nat
   | x :=
-    if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+    ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
 hash11 : Nat -> Nat
   | x :=
-    if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+    ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
 hash12 : Nat -> Nat
   | x :=
-    if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+    ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
 hash13 : Nat -> Nat
   | x :=
-    if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+    ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
 hash14 : Nat -> Nat
   | x :=
-    if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+    ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
 hash15 : Nat -> Nat
   | x :=
-    if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+    ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
 hash16 : Nat -> Nat
   | x :=
-    if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+    ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 hash : Nat -> Nat := hash16;
 
diff --git a/tests/Geb/positive/Compilation/test016.juvix b/tests/Geb/positive/Compilation/test016.juvix
index 3913c04c45..19c918b78e 100644
--- a/tests/Geb/positive/Compilation/test016.juvix
+++ b/tests/Geb/positive/Compilation/test016.juvix
@@ -8,10 +8,10 @@ f : Nat → Nat → Nat
   | x :=
     let
       g (y : Nat) : Nat := x + y;
-    in if
+    in ite
       (x == 0)
       (f 10)
-      (if (x < 10) λ {y := g (f (sub x 1) y)} g);
+      (ite (x < 10) λ {y := g (f (sub x 1) y)} g);
 
 g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
 
diff --git a/tests/Geb/positive/Compilation/test020.juvix b/tests/Geb/positive/Compilation/test020.juvix
index 0fd6c4a35a..ba9dcbf9dd 100644
--- a/tests/Geb/positive/Compilation/test020.juvix
+++ b/tests/Geb/positive/Compilation/test020.juvix
@@ -5,6 +5,6 @@ import Stdlib.Prelude open;
 
 terminating
 f91 : Nat → Nat
-  | n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
+  | n := ite (n > 100) (sub n 10) (f91 (f91 (n + 11)));
 
 main : Nat := f91 101 + f91 95 + f91 16 + f91 5;
diff --git a/tests/Geb/positive/Compilation/test021.juvix b/tests/Geb/positive/Compilation/test021.juvix
index 7ea78c4c43..a053f7cb1e 100644
--- a/tests/Geb/positive/Compilation/test021.juvix
+++ b/tests/Geb/positive/Compilation/test021.juvix
@@ -6,10 +6,10 @@ import Stdlib.Prelude open;
 terminating
 power' : Nat → Nat → Nat → Nat
   | acc a b :=
-    if
+    ite
       (b == 0)
       acc
-      (if
+      (ite
         (mod b 2 == 0)
         (power' acc (a * a) (div b 2))
         (power' (acc * a) (a * a) (div b 2)));
diff --git a/tests/Geb/positive/Compilation/test022.juvix b/tests/Geb/positive/Compilation/test022.juvix
index 9a1df8e3cc..3aa3a417bf 100644
--- a/tests/Geb/positive/Compilation/test022.juvix
+++ b/tests/Geb/positive/Compilation/test022.juvix
@@ -5,14 +5,14 @@ import Stdlib.Prelude open;
 
 terminating
 f : Nat → Nat
-  | x := if (x < 1) 1 (2 * x + g (sub x 1));
+  | x := ite (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
 g : Nat → Nat
-  | x := if (x < 1) 1 (x + h (sub x 1));
+  | x := ite (x < 1) 1 (x + h (sub x 1));
 
 terminating
 h : Nat → Nat
-  | x := if (x < 1) 1 (x * f (sub x 1));
+  | x := ite (x < 1) 1 (x * f (sub x 1));
 
 main : Nat := f 5 + f 10 + f 20;
diff --git a/tests/Geb/positive/Compilation/test023.juvix b/tests/Geb/positive/Compilation/test023.juvix
index 49e4bc26a5..6cd7e07907 100644
--- a/tests/Geb/positive/Compilation/test023.juvix
+++ b/tests/Geb/positive/Compilation/test023.juvix
@@ -6,7 +6,7 @@ import Stdlib.Prelude open;
 terminating
 gcd : Nat → Nat → Nat
   | a b :=
-    if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
+    ite (a > b) (gcd b a) (ite (a == 0) b (gcd (mod b a) a));
 
 main : Nat :=
   gcd (3 * 7 * 2) (7 * 2 * 11)
diff --git a/tests/Geb/positive/Compilation/test025.juvix b/tests/Geb/positive/Compilation/test025.juvix
index 83b1077aad..0803d8ac4d 100644
--- a/tests/Geb/positive/Compilation/test025.juvix
+++ b/tests/Geb/positive/Compilation/test025.juvix
@@ -9,7 +9,7 @@ pow : Nat -> Nat
 
 hash' : Nat -> Nat -> Nat
   | (suc n@(suc (suc m))) x :=
-    if
+    ite
       (x < pow n)
       (hash' n x)
       (mod (div (x * x) (pow m)) (pow 6))
diff --git a/tests/Geb/positive/Compilation/test026.juvix b/tests/Geb/positive/Compilation/test026.juvix
index 7d052f7c69..29080b4ed5 100644
--- a/tests/Geb/positive/Compilation/test026.juvix
+++ b/tests/Geb/positive/Compilation/test026.juvix
@@ -15,11 +15,11 @@ sum : Nat → Nat :=
 mutrec : Nat :=
   let
     terminating
-    f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
+    f (x : Nat) : Nat := ite (x < 1) 1 (g (sub x 1) + 2 * x);
     terminating
-    g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
+    g (x : Nat) : Nat := ite (x < 1) 1 (x + h (sub x 1));
     terminating
-    h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
+    h (x : Nat) : Nat := ite (x < 1) 1 (x * f (sub x 1));
   in f 5 + f 10 + g 5 + h 5;
 
 main : Nat := sum 100 + mutrec;
diff --git a/tests/Internal/Core/positive/test006.juvix b/tests/Internal/Core/positive/test006.juvix
index 19be5d2551..c8add85c19 100644
--- a/tests/Internal/Core/positive/test006.juvix
+++ b/tests/Internal/Core/positive/test006.juvix
@@ -5,7 +5,7 @@ import Stdlib.Prelude open;
 terminating
 loop : Nat := loop;
 
-e : Nat := (if (3 > 0) 1 loop) + (if (2 < 1) loop (if (7 >= 8) loop 1));
+e : Nat := (ite (3 > 0) 1 loop) + (ite (2 < 1) loop (ite (7 >= 8) loop 1));
 
 main : IO := printNatLn e;
 
diff --git a/tests/Internal/positive/BuiltinIf.juvix b/tests/Internal/positive/BuiltinIf.juvix
index 03aa0f5f92..839aa0f705 100644
--- a/tests/Internal/positive/BuiltinIf.juvix
+++ b/tests/Internal/positive/BuiltinIf.juvix
@@ -2,5 +2,5 @@ module BuiltinIf;
 
 import Stdlib.Prelude open;
 
-main : Bool := if false (and false) (and true) true;
+main : Bool := ite false (and false) (and true) true;
 
diff --git a/tests/Internal/positive/QuickSort.juvix b/tests/Internal/positive/QuickSort.juvix
index c19a9c1d70..fb5c664302 100644
--- a/tests/Internal/positive/QuickSort.juvix
+++ b/tests/Internal/positive/QuickSort.juvix
@@ -20,7 +20,7 @@ uniq
   | _ nil := nil
   | _ y@(x :: nil) := y
   | cmp (x :: x' :: xs) :=
-    if
+    ite
       (isEQ (cmp x x'))
       (uniq cmp (x' :: xs))
       (x :: uniq cmp (x' :: xs));
diff --git a/tests/Rust/Compilation/positive/test006.juvix b/tests/Rust/Compilation/positive/test006.juvix
index 2032d091a4..bc285cf1af 100644
--- a/tests/Rust/Compilation/positive/test006.juvix
+++ b/tests/Rust/Compilation/positive/test006.juvix
@@ -7,7 +7,7 @@ terminating
 loop : Nat := loop;
 
 main : Nat :=
-  if (3 > 0) 1 loop
-    + if (2 < 1) loop (if (7 >= 8) loop 1)
-    + if (2 > 0 || loop == 0) 1 0
-    + if (2 < 0 && loop == 0) 1 0;
+  ite (3 > 0) 1 loop
+    + ite (2 < 1) loop (ite (7 >= 8) loop 1)
+    + ite (2 > 0 || loop == 0) 1 0
+    + ite (2 < 0 && loop == 0) 1 0;
diff --git a/tests/Rust/Compilation/positive/test007.juvix b/tests/Rust/Compilation/positive/test007.juvix
index 998b804c07..b2c114dec7 100644
--- a/tests/Rust/Compilation/positive/test007.juvix
+++ b/tests/Rust/Compilation/positive/test007.juvix
@@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
 lst : List Nat := 0 :: 1 :: nil;
 
 main : Nat :=
-  if (null lst) 1 0
-    + if (null (nil {Nat})) 1 0
+  ite (null lst) 1 0
+    + ite (null (nil {Nat})) 1 0
     + head 1 lst
     + head 0 (tail lst)
     + head 0 (tail (map ((+) 1) lst))
diff --git a/tests/Rust/Compilation/positive/test013.juvix b/tests/Rust/Compilation/positive/test013.juvix
index b0d63c9a81..52544cb108 100644
--- a/tests/Rust/Compilation/positive/test013.juvix
+++ b/tests/Rust/Compilation/positive/test013.juvix
@@ -5,12 +5,12 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | x :=
-    if
+    ite
       (x == 6)
       λ {_ := 0}
-      (if
+      (ite
         (x == 5)
         λ {_ := 1}
-        (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
+        (ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
 
 main : Nat := f 5 6 + f 6 5 + f 10 5 + f 11 5;
diff --git a/tests/Rust/Compilation/positive/test015.juvix b/tests/Rust/Compilation/positive/test015.juvix
index 6c6486d628..43b5edea02 100644
--- a/tests/Rust/Compilation/positive/test015.juvix
+++ b/tests/Rust/Compilation/positive/test015.juvix
@@ -8,10 +8,10 @@ f : Nat → Nat → Nat
   | x :=
     let
       g (y : Nat) : Nat := x + y;
-    in if
+    in ite
       (x == 0)
       (f 10)
-      (if (x < 10) λ {y := g (f (sub x 1) y)} g);
+      (ite (x < 10) λ {y := g (f (sub x 1) y)} g);
 
 g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
 
diff --git a/tests/Rust/Compilation/positive/test020.juvix b/tests/Rust/Compilation/positive/test020.juvix
index 4cd552d220..64f6743095 100644
--- a/tests/Rust/Compilation/positive/test020.juvix
+++ b/tests/Rust/Compilation/positive/test020.juvix
@@ -6,12 +6,12 @@ import Stdlib.Prelude open;
 -- McCarthy's 91 function
 terminating
 f91 : Nat → Nat
-  | n := if (n > 100) (sub n 10) (f91 (f91 (n + 11)));
+  | n := ite (n > 100) (sub n 10) (f91 (f91 (n + 11)));
 
 -- subtraction by increments
 terminating
 subp : Nat → Nat → Nat
-  | i j := if (i == j) 0 (subp i (j + 1) + 1);
+  | i j := ite (i == j) 0 (subp i (j + 1) + 1);
 
 main : Nat :=
   f91 101
diff --git a/tests/Rust/Compilation/positive/test023.juvix b/tests/Rust/Compilation/positive/test023.juvix
index 26cb5429ab..0414f08853 100644
--- a/tests/Rust/Compilation/positive/test023.juvix
+++ b/tests/Rust/Compilation/positive/test023.juvix
@@ -6,14 +6,14 @@ import Stdlib.Prelude open;
 terminating
 f : Nat → Nat
 
-  | x := if (x < 1) 1 (2 * x + g (sub x 1));
+  | x := ite (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating
 g : Nat → Nat
-  | x := if (x < 1) 1 (x + h (sub x 1));
+  | x := ite (x < 1) 1 (x + h (sub x 1));
 
 terminating
 h : Nat → Nat
-  | x := if (x < 1) 1 (x * f (sub x 1));
+  | x := ite (x < 1) 1 (x * f (sub x 1));
 
 main : Nat := f 5 + f 10 + f 20;
diff --git a/tests/Rust/Compilation/positive/test024.juvix b/tests/Rust/Compilation/positive/test024.juvix
index 83d3acdda3..b5b5aaa213 100644
--- a/tests/Rust/Compilation/positive/test024.juvix
+++ b/tests/Rust/Compilation/positive/test024.juvix
@@ -15,7 +15,7 @@ gen : Nat → Tree
 g : Tree → Tree
 
   | leaf := leaf
-  | (node l r) := if (isNode l) r (node r l);
+  | (node l r) := ite (isNode l) r (node r l);
 
 terminating
 f : Tree → Nat
diff --git a/tests/Rust/Compilation/positive/test025.juvix b/tests/Rust/Compilation/positive/test025.juvix
index ceb84cd312..1e1d35ef3d 100644
--- a/tests/Rust/Compilation/positive/test025.juvix
+++ b/tests/Rust/Compilation/positive/test025.juvix
@@ -6,7 +6,7 @@ import Stdlib.Prelude open;
 terminating
 gcd : Nat → Nat → Nat
   | a b :=
-    if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
+    ite (a > b) (gcd b a) (ite (a == 0) b (gcd (mod b a) a));
 
 main : Nat :=
   gcd (3 * 7 * 2) (7 * 2 * 11)
diff --git a/tests/Rust/Compilation/positive/test026.juvix b/tests/Rust/Compilation/positive/test026.juvix
index f3cc2b1a6c..e91eafc367 100644
--- a/tests/Rust/Compilation/positive/test026.juvix
+++ b/tests/Rust/Compilation/positive/test026.juvix
@@ -43,7 +43,7 @@ empty : {A : Type} → Queue A := queue nil nil;
 terminating
 g {{Partial}} : List Nat → Queue Nat → List Nat
   | acc q :=
-    if (is_empty q) acc (g (front q :: acc) (pop_front q));
+    ite (is_empty q) acc (g (front q :: acc) (pop_front q));
 
 f {{Partial}} : Nat → Queue Nat → List Nat
   | zero q := g nil q
diff --git a/tests/Rust/Compilation/positive/test028.juvix b/tests/Rust/Compilation/positive/test028.juvix
index c014a3a584..26a73be327 100644
--- a/tests/Rust/Compilation/positive/test028.juvix
+++ b/tests/Rust/Compilation/positive/test028.juvix
@@ -12,7 +12,7 @@ terminating
 sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
   | p s unit :=
     case force s of {cons h t :=
-      if (p h) (cons h (sfilter p t)) (force (sfilter p t))};
+      ite (p h) (cons h (sfilter p t)) (force (sfilter p t))};
 
 shead : Stream → Nat
   | (cons h _) := h;
diff --git a/tests/Rust/Compilation/positive/test032.juvix b/tests/Rust/Compilation/positive/test032.juvix
index b6932d7ac9..f720d33828 100644
--- a/tests/Rust/Compilation/positive/test032.juvix
+++ b/tests/Rust/Compilation/positive/test032.juvix
@@ -14,14 +14,14 @@ merge' : List Nat → List Nat → List Nat
   | nil ys := ys
   | xs nil := xs
   | xs@(x :: xs') ys@(y :: ys') :=
-    if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
+    ite (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
 
 terminating
 sort : List Nat → List Nat
   | xs :=
     let
       n : Nat := length xs;
-    in if
+    in ite
       (n <= 1)
       xs
       case split (div n 2) xs of {l1, l2 :=
@@ -32,7 +32,7 @@ uniq : List Nat → List Nat
   | nil := nil
   | (x :: nil) := x :: nil
   | (x :: xs@(x' :: _)) :=
-    if (x == x') (uniq xs) (x :: uniq xs);
+    ite (x == x') (uniq xs) (x :: uniq xs);
 
 gen : List Nat → Nat → (Nat → Nat) → List Nat
   | acc zero f := acc
diff --git a/tests/Rust/Compilation/positive/test034.juvix b/tests/Rust/Compilation/positive/test034.juvix
index 6cfd93686b..562c4fc939 100644
--- a/tests/Rust/Compilation/positive/test034.juvix
+++ b/tests/Rust/Compilation/positive/test034.juvix
@@ -15,11 +15,11 @@ sum : Nat → Nat :=
 mutrec : Nat :=
   let
     terminating
-    f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x);
+    f (x : Nat) : Nat := ite (x < 1) 1 (g (sub x 1) + 2 * x);
     terminating
-    g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1));
+    g (x : Nat) : Nat := ite (x < 1) 1 (x + h (sub x 1));
     terminating
-    h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1));
+    h (x : Nat) : Nat := ite (x < 1) 1 (x * f (sub x 1));
   in f 5 + f 10 + g 5 + h 5;
 
 main : Nat := sum 1000 + mutrec;
diff --git a/tests/Rust/Compilation/positive/test039.juvix b/tests/Rust/Compilation/positive/test039.juvix
index 76d471bd28..c33d12f0cf 100644
--- a/tests/Rust/Compilation/positive/test039.juvix
+++ b/tests/Rust/Compilation/positive/test039.juvix
@@ -14,4 +14,4 @@ main : Nat :=
       | zero := true
       | (suc n) := not (odd n);
     plusOne (n : Ty) : Ty := n + 1;
-  in if (odd (plusOne 13)) 1 0 + if (even (plusOne 12)) 1 0;
+  in ite (odd (plusOne 13)) 1 0 + ite (even (plusOne 12)) 1 0;
diff --git a/tests/Rust/Compilation/positive/test040.juvix b/tests/Rust/Compilation/positive/test040.juvix
index 2d5fb89f25..039eac69c6 100644
--- a/tests/Rust/Compilation/positive/test040.juvix
+++ b/tests/Rust/Compilation/positive/test040.juvix
@@ -14,4 +14,4 @@ type Foo (A : Type) :=
 f : {A : Type} -> Foo A -> A
   | (foo unit a) := a;
 
-main : Nat := if (f (foo unit true)) 1 0;
+main : Nat := ite (f (foo unit true)) 1 0;
diff --git a/tests/Rust/Compilation/positive/test060.juvix b/tests/Rust/Compilation/positive/test060.juvix
index 7e352001f2..a7865ffaf0 100644
--- a/tests/Rust/Compilation/positive/test060.juvix
+++ b/tests/Rust/Compilation/positive/test060.juvix
@@ -34,7 +34,7 @@ main : Nat :=
       };
     f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
       (@Triple{fst := fst * 10});
-  in sum <| if
+  in sum <| ite
     (mf
       mkPair@{
         fst := mkPair true nil;
diff --git a/tests/Rust/Compilation/positive/test064.juvix b/tests/Rust/Compilation/positive/test064.juvix
index c3674c2730..17915e9e48 100644
--- a/tests/Rust/Compilation/positive/test064.juvix
+++ b/tests/Rust/Compilation/positive/test064.juvix
@@ -8,10 +8,10 @@ import Stdlib.Debug.Fail as Debug;
 f (x y : Nat) : Nat := x + y;
 
 {-# inline: false #-}
-g (x : Bool) : Bool := if x false true;
+g (x : Bool) : Bool := ite x false true;
 
 {-# inline: false #-}
-h (x : Bool) : Bool := if (g x) false true;
+h (x : Bool) : Bool := ite (g x) false true;
 
 {-# inline: false, eval: false #-}
 j (x : Nat) : Nat := x + 0;
@@ -37,6 +37,6 @@ even' : Nat -> Bool := even;
 main : Nat :=
   sum 3
     + case even' 6 || g true || h true of {
-        | true := if (g false) (f 1 2 + sum 7 + j 0) 0
+        | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
         | false := f (3 + 4) (f 0 8) + loop
       };
diff --git a/tests/Rust/Compilation/positive/test069.juvix b/tests/Rust/Compilation/positive/test069.juvix
index 0484d600d8..e5ec4e3f72 100644
--- a/tests/Rust/Compilation/positive/test069.juvix
+++ b/tests/Rust/Compilation/positive/test069.juvix
@@ -28,4 +28,4 @@ ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare);
 instance
 ordNat : Ord Nat := mkOrdHelper Ord.compare;
 
-main : Nat := if (Ord.lt 1 2) 1 0;
+main : Nat := ite (Ord.lt 1 2) 1 0;
diff --git a/tests/Rust/Compilation/positive/test071.juvix b/tests/Rust/Compilation/positive/test071.juvix
index d552c66825..f5bd48deb0 100644
--- a/tests/Rust/Compilation/positive/test071.juvix
+++ b/tests/Rust/Compilation/positive/test071.juvix
@@ -39,5 +39,5 @@ h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d;
 
 main : Nat :=
   fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} +
-  f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 +
+  f@{c := 5} + g@?{b := 4} 3 + ite (Ord.lt 1 0) 1 0 +
   h@?{b := 4} 1;
diff --git a/tests/VampIR/positive/Compilation/test001.juvix b/tests/VampIR/positive/Compilation/test001.juvix
index 69320a4ad3..4782c536c6 100644
--- a/tests/VampIR/positive/Compilation/test001.juvix
+++ b/tests/VampIR/positive/Compilation/test001.juvix
@@ -4,4 +4,4 @@ module test001;
 import Stdlib.Prelude open;
 
 main : Nat -> Nat
-  | x := if (x == 0) 1 0;
+  | x := ite (x == 0) 1 0;
diff --git a/tests/VampIR/positive/Compilation/test002.juvix b/tests/VampIR/positive/Compilation/test002.juvix
index 19c1718bf1..218e5fd5f1 100644
--- a/tests/VampIR/positive/Compilation/test002.juvix
+++ b/tests/VampIR/positive/Compilation/test002.juvix
@@ -8,17 +8,17 @@ type optbool :=
   | Nothing : optbool;
 
 natToBool : Nat -> Bool
-  | x := if (x == 0) false true;
+  | x := ite (x == 0) false true;
 
 boolToNat : Bool -> Nat
-  | x := if x 1 0;
+  | x := ite x 1 0;
 
 {-# public: [b] #-}
 main : Nat -> Nat -> Nat
   | a b :=
     boolToNat
       <| λ {
-          | x (Just b) := if x false b
+          | x (Just b) := ite x false b
           | _ Nothing := false
         }
         (natToBool a)
diff --git a/tests/VampIR/positive/Compilation/test003.juvix b/tests/VampIR/positive/Compilation/test003.juvix
index f6a9140755..31d2b9ae72 100644
--- a/tests/VampIR/positive/Compilation/test003.juvix
+++ b/tests/VampIR/positive/Compilation/test003.juvix
@@ -9,10 +9,10 @@ type enum :=
   | opt2 : Bool -> Bool -> enum;
 
 natToBool : Nat -> Bool
-  | x := if (x == 0) false true;
+  | x := ite (x == 0) false true;
 
 boolToNat : Bool -> Nat
-  | x := if x 1 0;
+  | x := ite x 1 0;
 
 main : Nat -> Nat -> Nat
   | x y :=
@@ -20,6 +20,6 @@ main : Nat -> Nat -> Nat
       <| λ {
           | opt0 := false
           | (opt1 b) := b
-          | (opt2 b c) := if b b c
+          | (opt2 b c) := ite b b c
         }
         (opt2 (natToBool x) (natToBool y));
diff --git a/tests/VampIR/positive/Compilation/test006.juvix b/tests/VampIR/positive/Compilation/test006.juvix
index e60168c198..3f0c3ba6b2 100644
--- a/tests/VampIR/positive/Compilation/test006.juvix
+++ b/tests/VampIR/positive/Compilation/test006.juvix
@@ -10,16 +10,16 @@ type enum :=
   | opt3 : Bool -> (Bool -> Bool -> Bool) -> Bool -> enum;
 
 natToBool : Nat -> Bool
-  | x := if (x == 0) false true;
+  | x := ite (x == 0) false true;
 
 boolToNat : Bool -> Nat
-  | x := if x 1 0;
+  | x := ite x 1 0;
 
 main : Nat -> Nat -> Nat
   | x y :=
     boolToNat
       <| case
-          opt3 (natToBool x) λ {x y := if y false x} (natToBool y)
+          opt3 (natToBool x) λ {x y := ite y false x} (natToBool y)
         of {
           | opt0 := false
           | opt1 b := b
diff --git a/tests/VampIR/positive/Compilation/test008.juvix b/tests/VampIR/positive/Compilation/test008.juvix
index e048afd352..5f4b1f82b2 100644
--- a/tests/VampIR/positive/Compilation/test008.juvix
+++ b/tests/VampIR/positive/Compilation/test008.juvix
@@ -5,13 +5,13 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | x :=
-    if
+    ite
       (x == 6)
       λ {_ := 0}
-      (if
+      (ite
         (x == 5)
         λ {_ := 1}
-        (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
+        (ite (x == 10) λ {_ := λ {x := x} 2} λ {x := x}));
 
 main : Nat -> Nat -> Nat
   | x y := f x (x + 1) + f (x + 1) x + f y x + f (y + 1) x;
diff --git a/tests/VampIR/positive/Compilation/test010.juvix b/tests/VampIR/positive/Compilation/test010.juvix
index 199fd2abb0..b811eecbdf 100644
--- a/tests/VampIR/positive/Compilation/test010.juvix
+++ b/tests/VampIR/positive/Compilation/test010.juvix
@@ -51,55 +51,55 @@ hash3 : Nat -> Nat
 
 hash4 : Nat -> Nat
   | x :=
-    if (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
+    ite (x < pow3) (hash3 x) (mod (div (x * x) pow1) pow6);
 
 hash5 : Nat -> Nat
   | x :=
-    if (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
+    ite (x < pow4) (hash4 x) (mod (div (x * x) pow2) pow6);
 
 hash6 : Nat -> Nat
   | x :=
-    if (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
+    ite (x < pow5) (hash5 x) (mod (div (x * x) pow3) pow6);
 
 hash7 : Nat -> Nat
   | x :=
-    if (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
+    ite (x < pow6) (hash6 x) (mod (div (x * x) pow4) pow6);
 
 hash8 : Nat -> Nat
   | x :=
-    if (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
+    ite (x < pow7) (hash7 x) (mod (div (x * x) pow5) pow6);
 
 hash9 : Nat -> Nat
   | x :=
-    if (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
+    ite (x < pow8) (hash8 x) (mod (div (x * x) pow6) pow6);
 
 hash10 : Nat -> Nat
   | x :=
-    if (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
+    ite (x < pow9) (hash9 x) (mod (div (x * x) pow7) pow6);
 
 hash11 : Nat -> Nat
   | x :=
-    if (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
+    ite (x < pow10) (hash10 x) (mod (div (x * x) pow8) pow6);
 
 hash12 : Nat -> Nat
   | x :=
-    if (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
+    ite (x < pow11) (hash11 x) (mod (div (x * x) pow9) pow6);
 
 hash13 : Nat -> Nat
   | x :=
-    if (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
+    ite (x < pow12) (hash12 x) (mod (div (x * x) pow10) pow6);
 
 hash14 : Nat -> Nat
   | x :=
-    if (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
+    ite (x < pow13) (hash13 x) (mod (div (x * x) pow11) pow6);
 
 hash15 : Nat -> Nat
   | x :=
-    if (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
+    ite (x < pow14) (hash14 x) (mod (div (x * x) pow12) pow6);
 
 hash16 : Nat -> Nat
   | x :=
-    if (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
+    ite (x < pow15) (hash15 x) (mod (div (x * x) pow13) pow6);
 
 {-# argnames: [val] #-}
 main : Nat -> Nat := hash16;
diff --git a/tests/VampIR/positive/Compilation/test022.juvix b/tests/VampIR/positive/Compilation/test022.juvix
index 83323e2943..37e306875f 100644
--- a/tests/VampIR/positive/Compilation/test022.juvix
+++ b/tests/VampIR/positive/Compilation/test022.juvix
@@ -9,8 +9,8 @@ power : Nat → Nat → Nat :=
     terminating
     power' (acc a b : Nat) : Nat :=
       let
-        acc' : Nat := if (mod b 2 == 0) acc (acc * a);
-      in if (b == 0) acc (power' acc' (a * a) (div b 2));
+        acc' : Nat := ite (mod b 2 == 0) acc (acc * a);
+      in ite (b == 0) acc (power' acc' (a * a) (div b 2));
   in power' 1;
 
 main : Nat -> Nat -> Nat := power;
diff --git a/tests/VampIR/positive/Compilation/test023.juvix b/tests/VampIR/positive/Compilation/test023.juvix
index a89af99bfc..00f98365a1 100644
--- a/tests/VampIR/positive/Compilation/test023.juvix
+++ b/tests/VampIR/positive/Compilation/test023.juvix
@@ -4,5 +4,5 @@ module test023;
 import Stdlib.Prelude open;
 
 main (x y : Nat) : Nat :=
-    case λ {z := if (x == z) (x, 0) (x, z)} (y + x) of
+    case λ {z := ite (x == z) (x, 0) (x, z)} (y + x) of
       a, b := a + b;
diff --git a/tests/benchmark/combinations/juvix/combinations.juvix b/tests/benchmark/combinations/juvix/combinations.juvix
index 0691f84d6d..56d2abacaa 100644
--- a/tests/benchmark/combinations/juvix/combinations.juvix
+++ b/tests/benchmark/combinations/juvix/combinations.juvix
@@ -8,7 +8,7 @@ go : Nat → Nat → Nat
   | _ zero := 1
   | zero _ := 0
   | n s :=
-    if
+    ite
       (s < n)
       (go (sub n 1) s)
       (go n (sub s n) + go (sub n 1) s);
diff --git a/tests/benchmark/mapfold/juvix/mapfold.juvix b/tests/benchmark/mapfold/juvix/mapfold.juvix
index 26db7626ed..7b83a29ab6 100644
--- a/tests/benchmark/mapfold/juvix/mapfold.juvix
+++ b/tests/benchmark/mapfold/juvix/mapfold.juvix
@@ -10,6 +10,6 @@ run : Nat → Nat → List Nat → Nat
 
 terminating
 gen : Nat → Nat → List Nat
-  | k n := if (k == n) (k :: nil) (k :: gen (suc k) n);
+  | k n := ite (k == n) (k :: nil) (k :: gen (suc k) n);
 
 main : IO := printNatLn (run 10000 0 (gen 1 10000));
diff --git a/tests/benchmark/mapfun/juvix/mapfun.juvix b/tests/benchmark/mapfun/juvix/mapfun.juvix
index 8e193879f9..6dd6173058 100644
--- a/tests/benchmark/mapfun/juvix/mapfun.juvix
+++ b/tests/benchmark/mapfun/juvix/mapfun.juvix
@@ -26,7 +26,7 @@ sum : List Int → Int := sum_go 0;
 
 terminating
 gen : Int → Int → List Int
-  | k n := if (k == n) (k :: nil) (k :: gen (k + 1) n);
+  | k n := ite (k == n) (k :: nil) (k :: gen (k + 1) n);
 
 main : IO :=
   printIntLn
diff --git a/tests/benchmark/maybe/juvix/maybe.juvix b/tests/benchmark/maybe/juvix/maybe.juvix
index 6f8dd620f8..232318e95b 100644
--- a/tests/benchmark/maybe/juvix/maybe.juvix
+++ b/tests/benchmark/maybe/juvix/maybe.juvix
@@ -18,7 +18,7 @@ terminating
 sum : Nat → Tree → Maybe Nat
   | x leaf := just 0
   | x (node y l r) :=
-    if (x == y) nothing (step1 x y (sum x l) r);
+    ite (x == y) nothing (step1 x y (sum x l) r);
 
 step2 : Nat → Maybe Nat → Maybe Nat
   | x (just y) := just (x + y)
diff --git a/tests/benchmark/mergesort/juvix/mergesort.juvix b/tests/benchmark/mergesort/juvix/mergesort.juvix
index 05afda83db..9ed7e7e33b 100644
--- a/tests/benchmark/mergesort/juvix/mergesort.juvix
+++ b/tests/benchmark/mergesort/juvix/mergesort.juvix
@@ -19,7 +19,7 @@ merget : List Nat → List Nat → List Nat → List Nat
   | nil ys acc := revappend acc ys
   | xs nil acc := revappend acc xs
   | (x :: xs') (y :: ys') acc :=
-    if
+    ite
       (x <= y)
       (merget xs' (y :: ys') (x :: acc))
       (merget (x :: xs') ys' (y :: acc));
@@ -37,14 +37,14 @@ sort : List Nat → List Nat
 sorted : List Nat → Bool
   | nil := true
   | (_ :: nil) := true
-  | (x :: y :: t) := if (x <= y) (sorted (y :: t)) false;
+  | (x :: y :: t) := ite (x <= y) (sorted (y :: t)) false;
 
 gen : Nat → List Nat → List Nat
   | zero acc := acc
   | (suc n) acc := gen n (suc n :: acc);
 
 main : IO :=
-  if
+  ite
     (sorted (sort (gen 2000000 nil)))
     (printStringLn "true")
     (printStringLn "false");
diff --git a/tests/benchmark/prime/juvix/prime.juvix b/tests/benchmark/prime/juvix/prime.juvix
index c21efb74cf..c741d39e98 100644
--- a/tests/benchmark/prime/juvix/prime.juvix
+++ b/tests/benchmark/prime/juvix/prime.juvix
@@ -5,14 +5,14 @@ import Stdlib.Prelude open;
 
 checkDivisible : Nat → List Nat → Bool
   | p nil := false
-  | p (h :: t) := if (mod p h == 0) true (checkDivisible p t);
+  | p (h :: t) := ite (mod p h == 0) true (checkDivisible p t);
 
 terminating
 go (n p : Nat) (lst : List Nat) : Nat :=
-    if
+    ite
       (n == 0)
       (head 0 lst)
-      (if
+      (ite
         (checkDivisible p lst)
         (go n (p + 1) lst)
         (go (sub n 1) (p + 1) (p :: lst)));
diff --git a/tests/negative/230/Foo/Data/Bool.juvix b/tests/negative/230/Foo/Data/Bool.juvix
index 022ca0441d..2c9173c01c 100644
--- a/tests/negative/230/Foo/Data/Bool.juvix
+++ b/tests/negative/230/Foo/Data/Bool.juvix
@@ -24,6 +24,6 @@ syntax operator && logical;
   | false _ := false
   | true a := a;
 
-if : {A : Type} → Bool → A → A → A
+ite : {A : Type} → Bool → A → A → A
   | true a _ := a
   | false _ b := b;
diff --git a/tests/negative/Internal/LazyBuiltin.juvix b/tests/negative/Internal/LazyBuiltin.juvix
index fb2d6274e5..cb23733771 100644
--- a/tests/negative/Internal/LazyBuiltin.juvix
+++ b/tests/negative/Internal/LazyBuiltin.juvix
@@ -6,9 +6,9 @@ type Bool :=
   | false : Bool;
 
 builtin bool-if
-if : {A : Type} -> Bool -> A -> A -> A
+ite : {A : Type} -> Bool -> A -> A -> A
   | true x _ := x
   | false _ x := x;
 
 f : Bool -> Bool
-  | x := if x;
+  | x := ite x;
diff --git a/tests/positive/BuiltinsBool.juvix b/tests/positive/BuiltinsBool.juvix
index 11676bfe52..2af59e2656 100644
--- a/tests/positive/BuiltinsBool.juvix
+++ b/tests/positive/BuiltinsBool.juvix
@@ -6,6 +6,6 @@ type Bool :=
   | false : Bool;
 
 builtin bool-if
-if : {A : Type} → Bool → A → A → A
+ite : {A : Type} → Bool → A → A → A
   | true t _ := t
   | false _ e := e;
diff --git a/tests/positive/Format.juvix b/tests/positive/Format.juvix
index af14283a82..ccaf0fa5c8 100644
--- a/tests/positive/Format.juvix
+++ b/tests/positive/Format.juvix
@@ -17,7 +17,7 @@ terminating
 -- Comment between terminating and type sig
 go : Nat → Nat → Nat
   | n s :=
-    if
+    ite
       (s < n)
       (go (sub n 1) s)
       (go n (sub s n) + go (sub n 1) s);
@@ -297,7 +297,7 @@ module Traits;
 
   instance
   showBoolI : Show Bool :=
-    mkShow (show := λ {x := if x "true" "false"});
+    mkShow (show := λ {x := ite x "true" "false"});
 
   instance
   showNatI : Show Nat := mkShow (show := natToString);
diff --git a/tests/positive/Internal/Implicit.juvix b/tests/positive/Internal/Implicit.juvix
index 6fd6011454..a02ded4b6d 100644
--- a/tests/positive/Internal/Implicit.juvix
+++ b/tests/positive/Internal/Implicit.juvix
@@ -65,7 +65,7 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-if : {A : Type} → Bool → A → A → A
+ite : {A : Type} → Bool → A → A → A
   | true a _ := a
   | false _ b := b;
 
@@ -130,10 +130,10 @@ foldl
 
 filter : {A : Type} → (A → Bool) → List A → List A
   | _ nil := nil
-  | f (h :: hs) := if (f h) (h :: filter f hs) (filter f hs);
+  | f (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs);
 
 partition
   : {A : Type} → (A → Bool) → List A → List A × List A
   | _ nil := nil, nil
   | f (x :: xs) :=
-    if (f x) first second ((::) x) (partition f xs);
+    ite (f x) first second ((::) x) (partition f xs);
diff --git a/tests/positive/Internal/Lambda.juvix b/tests/positive/Internal/Lambda.juvix
index 208f9b0f6c..388c38e9dc 100644
--- a/tests/positive/Internal/Lambda.juvix
+++ b/tests/positive/Internal/Lambda.juvix
@@ -118,7 +118,7 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-if : {A : Type} → Bool → A → A → A :=
+ite : {A : Type} → Bool → A → A → A :=
   λ {
     | true a _ := a
     | false _ b := b
@@ -127,7 +127,7 @@ if : {A : Type} → Bool → A → A → A :=
 filter : {A : Type} → (A → Bool) → List A → List A :=
   λ {
     | _ nil := nil
-    | f (h :: hs) := if (f h) (h :: filter f hs) (filter f hs)
+    | f (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs)
   };
 
 partition
@@ -135,7 +135,7 @@ partition
   λ {
     | _ nil := nil, nil
     | f (x :: xs) :=
-      if (f x) first second ((::) x) (partition f xs)
+      ite (f x) first second ((::) x) (partition f xs)
   };
 
 zipWith
diff --git a/tests/positive/issue1731/builtinTrace.juvix b/tests/positive/issue1731/builtinTrace.juvix
index e6234a03d6..29aee9c7af 100644
--- a/tests/positive/issue1731/builtinTrace.juvix
+++ b/tests/positive/issue1731/builtinTrace.juvix
@@ -7,7 +7,7 @@ axiom trace : {A : Type} → A → A;
 
 terminating
 f : Nat → Nat → Nat
-  | x y := if (x == 0) y (trace x >-> f (sub x 1) y);
+  | x y := ite (x == 0) y (trace x >-> f (sub x 1) y);
 
 {-
 f 4 0 =