Use multiway if in the standard library

Stdlib/Cairo/Ec.juvix

@@ -44,39 +44,38 @@ end;
 isOnCurve : Point -> Bool
   | (mkPoint x y) :=
     if
-      (y == 0)
-      (x == 0)
-      (y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA);
+      | y == 0 := x == 0
+      | else :=
+        y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
 
 --- Doubles a valid point p (computes p + p) on the elliptic curve.
 double : Point -> Point
   | p@(mkPoint x y) :=
     if
-      (y == 0)
-      p
-      (let
-        slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y);
-        r_x := slope * slope - x - x;
-        r_y := slope * (x - r_x) - y;
-      in mkPoint (x := r_x; y := r_y));
+      | y == 0 := p
+      | else :=
+        let
+          slope := (3 * x * x + StarkCurve.ALPHA) / (2 * y);
+          r_x := slope * slope - x - x;
+          r_y := slope * (x - r_x) - y;
+        in mkPoint (x := r_x; y := r_y);
 
 --- Adds two valid points on the EC.
 add : Point -> Point -> Point
   | p@(mkPoint x1 y1) q@(mkPoint x2 y2) :=
     if
-      (y1 == 0)
-      q
-      (if
-        (y2 == 0)
-        p
-        (if
-          (x1 == x2)
-          (if (y1 == y2) (double p) (mkPoint 0 0))
-          (let
-            slope := (y1 - y2) / (x1 - x2);
-            r_x := slope * slope - x1 - x2;
-            r_y := slope * (x1 - r_x) - y1;
-          in mkPoint r_x r_y)));
+      | y1 == 0 := q
+      | y2 == 0 := p
+      | x1 == x2 :=
+        if
+          | y1 == y2 := double p
+          | else := mkPoint 0 0
+      | else :=
+        let
+          slope := (y1 - y2) / (x1 - x2);
+          r_x := slope * slope - x1 - x2;
+          r_y := slope * (x1 - r_x) - y1;
+        in mkPoint r_x r_y;
 
 --- Subtracts a point from another on the EC.
 sub (p q : Point) : Point := add p q@Point{y := 0 - y};
@@ -102,12 +101,12 @@ sub (p q : Point) : Point := add p q@Point{y := 0 - y};
 --- p and q are valid points on the curve.
 addMul (p : Point) (m : Field) (q : Point) : Point :=
   if
-    (Point.y q == 0)
-    p
-    (let
-      s : Point := Internal.randomEcPoint;
-      r : Point := Internal.ecOp (add p s) m q;
-    in sub r s);
+    | Point.y q == 0 := p
+    | else :=
+      let
+        s : Point := Internal.randomEcPoint;
+        r : Point := Internal.ecOp (add p s) m q;
+      in sub r s;
 
 --- Computes m * p on the elliptic curve.
 mul (m : Field) (p : Point) : Point :=

Stdlib/Data/Int/Ord.juvix

@@ -48,7 +48,10 @@ syntax operator >= comparison;
 --- Tests for ;Ordering;.
 {-# inline: true #-}
 compare (m n : Int) : Ordering :=
-  if (m == n) EQ (if (m < n) LT GT);
+  if
+    | m == n := EQ
+    | m < n := LT
+    | else := GT;
 
 --- Returns the smallest ;Int;.
 min (x y : Int) : Int := if (x < y) x y;

Stdlib/Data/List/Base.juvix

@@ -94,9 +94,8 @@ terminating
 merge {A} {{Ord A}} : List A → List A → List A
   | xs@(x :: xs') ys@(y :: ys') :=
     if
-      (isLT (Ord.cmp x y))
-      (x :: merge xs' ys)
-      (y :: merge xs ys')
+      | isLT (Ord.cmp x y) := x :: merge xs' ys
+      | else := y :: merge xs ys'
   | nil ys := ys
   | xs nil := xs;
 

Stdlib/Data/Nat/Ord.juvix

@@ -49,7 +49,10 @@ syntax operator >= comparison;
 --- Tests for ;Ordering;.
 {-# inline: true #-}
 compare (n m : Nat) : Ordering :=
-  if (n == m) EQ (if (n < m) LT GT);
+  if
+    | n == m := EQ
+    | n < m := LT
+    | else := GT;
 
 --- Returns the smaller ;Nat;.
 min (x y : Nat) : Nat := if (x < y) x y;