Skip to content

Commit

Permalink
rename if to ite
Browse files Browse the repository at this point in the history
  • Loading branch information
janmasrovira committed Jun 26, 2024
1 parent 00f6f50 commit 50acdf1
Show file tree
Hide file tree
Showing 8 changed files with 15 additions and 15 deletions.
2 changes: 1 addition & 1 deletion Stdlib/Data/Bool/Base.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
4 changes: 2 additions & 2 deletions Stdlib/Data/Int/Ord.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
2 changes: 1 addition & 1 deletion Stdlib/Data/List.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions Stdlib/Data/List/Base.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions Stdlib/Data/Nat/Ord.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
2 changes: 1 addition & 1 deletion Stdlib/Data/Range.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions Stdlib/Extra/Gcd.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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);
4 changes: 2 additions & 2 deletions Stdlib/Trait/Ord.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -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;

0 comments on commit 50acdf1

Please sign in to comment.