format juvix files

tests/negative/issue1337/DoubleBraces.juvix

@@ -4,4 +4,4 @@ type Nat :=
   | O : Nat
   | S : Nat -> Nat;
 
-fun (n : Nat) : Nat := case n of {S {{y}} := O};
+fun (n : Nat) : Nat := case n of S {{y}} := O;

tests/positive/Alias.juvix

@@ -20,10 +20,9 @@ not2 (b : Boolean) : Boolean :=
   let
     syntax alias yes := ⊤;
     syntax alias no := ⊥;
-  in case b of {
+  in case b of
        | no := yes
-       | yes := no
-     };
+       | yes := no;
 
 module ExportAlias;
   syntax alias Binary := Bool;

tests/positive/AliasRecordConstructor.juvix

@@ -12,7 +12,7 @@ t : T :=
   };
 
 t1 : T -> A
- | mkT'@{ field := x } := x;
+  | mkT'@{field := x} := x;
 
 syntax iterator it {init := 0; range := 1};
 it : (A → A) → T → A

tests/positive/Format.juvix

@@ -30,31 +30,28 @@ M;
 end;
 
 -- case with single branch
-case1 (n : Nat) : Nat := case n of {x := zero};
+case1 (n : Nat) : Nat := case n of x := zero;
 
 -- case with multiple branches
 case2 (n : Nat) : Nat :=
-  case n of {
+  case n of
     | zero := zero
-    | _ := zero
-  };
+    | _ := zero;
 
 -- case on nested case
 case3 (n : Nat) : Nat :=
-  case case n of {_ := zero} of {
+  case case n of {_ := zero} of
     | zero := zero
-    | _ := zero
-  };
+    | _ := zero;
 
 -- case on nested case expression
 case4 (n : Nat) : Nat :=
-  case n of {
+  case n of
     | zero := case n of {x := zero}
-    | _ := zero
-  };
+    | _ := zero;
 
 -- -- case with application subject
-case5 (n : Nat) : Nat := case id n of {x := zero};
+case5 (n : Nat) : Nat := case id n of x := zero;
 
 -- qualified commas
 t4 : String := "a" M., "b" M., "c" M., "d";

tests/positive/ImportShadow/Main.juvix

@@ -4,13 +4,12 @@ import Nat open;
 
 type Unit := unit : Unit;
 
-f : Nat := case unit of {is-zero := zero};
+f : Nat := case unit of is-zero := zero;
 
 f2 : Nat :=
-  case suc zero of {
+  case suc zero of
     | suc is-zero := zero
-    | _ := zero
-  };
+    | _ := zero;
 
 f3 : Nat → Nat
   | (suc is-zero) := is-zero

tests/positive/ImportShadow/Nat.juvix

@@ -10,7 +10,6 @@ type Nat :=
 
 is-zero : Nat → Bool
   | n :=
-    case n of {
+    case n of
       | zero := true
-      | suc _ := false
-    };
+      | suc _ := false;

tests/positive/InstanceImport/Main.juvix

@@ -10,4 +10,4 @@ type Bool :=
 instance
 boolI : T Bool := mkT λ {x := x};
 
-main : Bool := case T.pp unit of {unit := T.pp true};
+main : Bool := case T.pp unit of unit := T.pp true;

tests/positive/Iterators.juvix

@@ -19,7 +19,6 @@ main : Bool :=
     z : Bool := false;
   in itconst (a := true; b := false) (c in false; d in false)
        for (x := true) (y in false)
-         case x of {
+         case x of
            | true := y
-           | false := z
-         };
+           | false := z;

tests/positive/LetShadow.juvix

@@ -7,9 +7,8 @@ type Nat :=
 type Unit := unit : Unit;
 
 t : Nat :=
-  case unit of {
+  case unit of
     x :=
       let
         x : Nat := suc zero;
-      in x
-  };
+      in x;

tests/positive/NestedPatterns.juvix

@@ -9,7 +9,6 @@ toList : {A : Type} -> MyList A -> List A
 
 f : MyList Nat -> Nat
   | xs :=
-    case toList xs of {
+    case toList xs of
       | suc n :: nil := n
-      | _ := zero
-    };
+      | _ := zero;

tests/positive/Traits2.juvix

@@ -79,7 +79,7 @@ import Stdlib.Data.Product open;
   {{Semigroup A}}
   {B C : Type}
   : A × B -> (B -> A × C) -> A × C
-  | (a, b) f := case f b of {a', b' := a <> a', b'};
+  | (a, b) f := case f b of a', b' := a <> a', b';
 
 instance
 ×-Monad