diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix index 79578322..a4dad773 100644 --- a/Stdlib/Data/Bool/Base.juvix +++ b/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; diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix index bc62cf5f..31fdf058 100644 --- a/Stdlib/Data/Int/Ord.juvix +++ 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; diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix index 0dd534fb..67128654 100644 --- a/Stdlib/Data/List.juvix +++ b/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 diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix index 53aa4bf4..258fb67b 100644 --- a/Stdlib/Data/List/Base.juvix +++ b/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,7 +147,7 @@ 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}; @@ -155,7 +155,7 @@ syntax iterator all {init := 0; range := 1}; {-# 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 diff --git a/Stdlib/Data/Nat/Ord.juvix b/Stdlib/Data/Nat/Ord.juvix index 24b91ed1..c97c6290 100644 --- a/Stdlib/Data/Nat/Ord.juvix +++ b/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; diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix index 8b2089ce..45c0a01f 100644 --- a/Stdlib/Data/Range.juvix +++ b/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; diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix index cfcc5300..4383431f 100644 --- a/Stdlib/Extra/Gcd.juvix +++ b/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); diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix index 8b777538..6406e382 100644 --- a/Stdlib/Trait/Ord.juvix +++ 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;