Format stdlib

Stdlib/Data/Int/Base.juvix

@@ -28,9 +28,10 @@ nonNeg : Int -> Bool
 --- Subtraction for ;Nat;s.
 builtin int-sub-nat
 intSubNat (n m : Nat) : Int :=
-  case sub n m
+  case sub n m of {
     | zero := ofNat (Nat.sub m n)
-    | suc k := negSuc k;
+    | suc k := negSuc k
+  };
 
 syntax operator + additive;
 

Stdlib/Data/Int/Range.juvix

@@ -8,11 +8,11 @@ import Stdlib.Data.Int.Ord open;
 
 --- A range of integers
 type Range :=
-  | mkRange {
-      low : Int;
-      high : Int;
-      step : Int
-    };
+  mkRange {
+    low : Int;
+    high : Int;
+    step : Int
+  };
 
 syntax iterator for {init: 1, range: 1};
 

Stdlib/Data/List.juvix

@@ -32,10 +32,11 @@ ordListI {A} {{Ord A}} : Ord (List A) :=
       | nil _ := LT
       | _ nil := GT
       | (x :: xs) (y :: ys) :=
-        case Ord.cmp x y
+        case Ord.cmp x y of {
           | LT := LT
           | GT := GT
-          | EQ := go xs ys;
+          | EQ := go xs ys
+        };
   in mkOrd go;
 
 instance

Stdlib/Data/List/Base.juvix

@@ -97,8 +97,7 @@ splitAt {A} : Nat → List A → List A × List A
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
   | (suc m) (x :: xs) :=
-    case splitAt m xs
-      | l1, l2 := x :: l1, l2;
+    case splitAt m xs of {l1, l2 := x :: l1, l2};
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
 merge {A} : Ord A → List A → List A → List A
@@ -115,8 +114,8 @@ merge {A} : Ord A → List A → List A → List A
 partition {A} (f : A → Bool) : List A → List A × List A
   | nil := nil, nil
   | (x :: xs) :=
-    case partition f xs
-      | l1, l2 := if (f x) (x :: l1, l2) (l1, x :: l2);
+    case partition f xs of {l1, l2 :=
+      if (f x) (x :: l1, l2) (l1, x :: l2)};
 
 syntax operator ++ cons;
 
@@ -211,8 +210,8 @@ quickSort {A} : Ord A → List A → List A
         | nil := nil
         | xs@(_ :: nil) := xs
         | (x :: xs) :=
-          case partition (isGT ∘ cmp x) xs
-            | l1, l2 := go l1 ++ x :: go l2;
+          case partition (isGT ∘ cmp x) xs of {l1, l2 :=
+            go l1 ++ x :: go l2};
     in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.

Stdlib/Data/Nat/Range.juvix

@@ -8,11 +8,11 @@ import Stdlib.Data.Nat.Ord open;
 
 --- A range of natural numbers
 type Range :=
-  | mkRange {
-      low : Nat;
-      high : Nat;
-      step : Nat
-    };
+  mkRange {
+    low : Nat;
+    high : Nat;
+    step : Nat
+  };
 
 syntax iterator for {init: 1, range: 1};
 

Stdlib/Data/Product.juvix

@@ -18,10 +18,11 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (A × B)
   | {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=
     mkOrd
       λ {(a1, b1) (a2, b2) :=
-        case cmp-a a1 a2
+        case cmp-a a1 a2 of {
           | LT := LT
           | GT := GT
-          | EQ := cmp-b b1 b2};
+          | EQ := cmp-b b1 b2
+        }};
 
 instance
 showProductI {A B}

Stdlib/Data/Product/Base.juvix

@@ -6,8 +6,7 @@ syntax operator × functor;
 syntax operator , pair;
 
 --- Inductive pair. I.e. a tuple with two components.
-type × (A B : Type) :=
-  | , : A → B → A × B;
+type × (A B : Type) := , : A → B → A × B;
 
 --- Converts a function of two arguments to a function with a product argument.
 uncurry {A B C} (f : A -> B -> C) : A × B -> C

test/Test.juvix

@@ -33,10 +33,9 @@ prop-splitAtRecombine : Nat -> List Int -> Bool
 
 prop-splitAtLength : Nat -> List Int -> Bool
   | n xs :=
-    case
-      splitAt
-        n
-        (xs ++ replicate (sub n (length xs)) (ofNat 0)) of {lhs
+    case splitAt
+      n
+      (xs ++ replicate (sub n (length xs)) (ofNat 0)) of {lhs
       , rhs :=
       length lhs Nat.== n
         && length rhs Nat.== sub (length xs) n};