fix formatting

examples/milestone/Hanoi/Hanoi.juvix

@@ -44,8 +44,8 @@ type Move :=
     to : Peg
   };
 
-showMove (move : Move) : String
- := showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move);
+showMove (move : Move) : String :=
+  showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move);
 
 --- Produce a list of ;Move;s that solves the towers of Hanoi game
 hanoi : Nat -> Peg -> Peg -> Peg -> List Move

tests/positive/265/M.juvix

@@ -4,8 +4,7 @@ type Bool :=
   | true : Bool
   | false : Bool;
 
-type Pair (A : Type) (B : Type) :=
-  mkPair : A → B → Pair A B;
+type Pair (A : Type) (B : Type) := mkPair : A → B → Pair A B;
 
 f : _ → _
   | (mkPair false true) := true

tests/positive/Internal/Positivity/RoseTree.juvix

@@ -4,5 +4,4 @@ type List (A : Type) : Type :=
   | nil : List A
   | cons : A -> List A -> List A;
 
-type RoseTree (A : Type) : Type :=
-  node : A -> List (RoseTree A) -> RoseTree A;
+type RoseTree (A : Type) : Type := node : A -> List (RoseTree A) -> RoseTree A;

tests/positive/Internal/Positivity2/main.juvix

@@ -10,6 +10,7 @@ type Box (A : Type) := box A;
 
 module M1;
   type T1 (x y : Type) := mkT1 y (x -> x) x;
+
   type T2 (x : (Type -> Type) -> Type) := mkT2 (x (T1 T));
 end;
 
@@ -18,7 +19,7 @@ module M2;
 
   type T2 (x : Type) := mkT2 (x -> T);
 
-  -- type T3 := mkT3 (T1 T3);
+-- type T3 := mkT3 (T1 T3);
 end;
 
 module M3;
@@ -40,11 +41,11 @@ module E3;
 end;
 
 module E5;
-  type Ghost1 (A : Type) := ghost1 (Ghost2 ((Ghost1 (A -> A)) -> Ghost2 A));
+  type Ghost1 (A : Type) := ghost1 (Ghost2 (Ghost1 (A -> A) -> Ghost2 A));
 
   type Ghost2 (B : Type) := ghost2 Ok (Ghost1 B);
 
-  type Ok  := mkOk (Ghost1 (Ok -> Ok));
+  type Ok := mkOk (Ghost1 (Ok -> Ok));
 end;
 
 module E6;

tests/positive/Isabelle/Program.juvix

@@ -12,7 +12,7 @@ id2 {A : Type} : A -> A := id;
 add_one : List Nat -> List Nat
   | [] := []
   -- hello!
-  | (x :: xs) := (x + 1) :: add_one xs;
+  | (x :: xs) := x + 1 :: add_one xs;
 
 sum : List Nat -> Nat
   | [] := 0
@@ -37,14 +37,20 @@ dec : Nat -> Nat
 dec' (x : Nat) : Nat :=
   -- Do case switch
   -- pattern match on x
-  case x of {- the zero case -} zero := {- return zero -} zero | {- the suc case -} suc y := y;
+  case x of
+    | {- the zero case -}
+    zero :=
+      {- return zero -}
+      zero
+    | {- the suc case -}
+    suc y := y;
 
 optmap {A} (f : A -> A) : Maybe A -> Maybe A
   | nothing := nothing
   | (just x) := just (f x);
 
 pboth {A B A' B'} (f : A -> A') (g : B -> B') : Pair A B -> Pair A' B'
-  | (x, y) := (f x, g y);
+  | (x, y) := f x, g y;
 
 bool_fun (x y z : Bool) : Bool := x && y || z;
 
@@ -62,26 +68,26 @@ qsnd : {A : Type} → Queue A → List A
   | (queue _ v) := v;
 
 pop_front {A} (q : Queue A) : Queue A :=
-    let
-      q' : Queue A := queue (tail (qfst q)) (qsnd q);
-    in case qfst q' of
-         | nil := queue (reverse (qsnd q')) nil
-         | _ := q';
+  let
+    q' : Queue A := queue (tail (qfst q)) (qsnd q);
+  in case qfst q' of
+       | nil := queue (reverse (qsnd q')) nil
+       | _ := q';
 
 push_back {A} (q : Queue A) (x : A) : Queue A :=
-    case qfst q of
-      | nil := queue (x :: nil) (qsnd q)
-      | q' := queue q' (x :: qsnd q);
+  case qfst q of
+    | nil := queue (x :: nil) (qsnd q)
+    | q' := queue q' (x :: qsnd q);
 
 --- Checks if the queue is empty
 is_empty {A} (q : Queue A) : Bool :=
-    case qfst q of
-      | nil :=
-        case qsnd q of {
-          | nil := true
-          | _ := false
-        }
-      | _ := false;
+  case qfst q of
+    | nil :=
+      case qsnd q of {
+        | nil := true
+        | _ := false
+      }
+    | _ := false;
 
 empty : {A : Type} → Queue A := queue nil nil;
 
@@ -96,52 +102,85 @@ funkcja (n : Nat) : Nat :=
 
 --- An Either' type
 type Either' A B :=
-  --- Left constructor
-  Left' A
-| --- Right constructor
-  Right' B;
+  | --- Left constructor
+    Left' A
+  | --- Right constructor
+    Right' B;
 
 -- Records
 
 {-# isabelle-ignore: true #-}
-type R' := mkR' {
-  r1' : Nat;
-  r2' : Nat;
-};
-
-type R := mkR {
-  r1 : Nat;
-  r2 : Nat;
-};
+type R' :=
+  mkR' {
+    r1' : Nat;
+    r2' : Nat
+  };
+
+type R :=
+  mkR {
+    r1 : Nat;
+    r2 : Nat
+  };
 
 r : R := mkR 0 1;
+
 v : Nat := 0;
 
-funR (r : R) : R :=
-  case r of
-  | mkR@{r1; r2} := r@R{r1 := r1 + r2};
+funR (r : R) : R := case r of mkR@{r1; r2} := r@R{r1 := r1 + r2};
 
 funRR : R -> R
   | r@mkR@{r1; r2} := r@R{r1 := r1 + r2};
 
 funR' : R -> R
-  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr1 + rr2; r2 := rr2};
+  | mkR@{r1 := rr1; r2 := rr2} :=
+    mkR@{
+      r1 := rr1 + rr2;
+      r2 := rr2
+    };
 
 funR1 : R -> R
-  | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
-  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1};
+  | mkR@{r1 := zero; r2} :=
+    mkR@{
+      r1 := r2;
+      r2
+    }
+  | mkR@{r1 := rr1; r2 := rr2} :=
+    mkR@{
+      r1 := rr2;
+      r2 := rr1
+    };
 
 funR2 (r : R) : R :=
   case r of
-  | mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
-  | mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1};
+    | mkR@{r1 := zero; r2} :=
+      mkR@{
+        r1 := r2;
+        r2
+      }
+    | mkR@{r1 := rr1; r2 := rr2} :=
+      mkR@{
+        r1 := rr2;
+        r2 := rr1
+      };
 
 funR3 (er : Either' R R) : R :=
   case er of
-  | Left' mkR@{r1 := zero; r2} := mkR@{r1 := r2; r2}
-  | Left' mkR@{r1 := rr1; r2 := rr2} := mkR@{r1 := rr2; r2 := rr1}
-  | Right' mkR@{r1; r2 := zero} := mkR@{r1 := 7; r2 := r1}
-  | Right' r@(mkR@{r1; r2}) := r@R{r1 := r2 + 2; r2 := r1 + 3};
+    | Left' mkR@{r1 := zero; r2} :=
+      mkR@{
+        r1 := r2;
+        r2
+      }
+    | Left' mkR@{r1 := rr1; r2 := rr2} :=
+      mkR@{
+        r1 := rr2;
+        r2 := rr1
+      }
+    | Right' mkR@{r1; r2 := zero} :=
+      mkR@{
+        r1 := 7;
+        r2 := r1
+      }
+    | Right' r@mkR@{r1; r2} := r@R{   r1 := r2 + 2; r2 := r1 + 3 };
 
 funR4 : R -> R
   | r@mkR@{r1} := r@R{r2 := r1};

tests/positive/MarkdownImport/B.juvix.md

@@ -1,5 +1,3 @@
-```juvix
 module B;
 
-axiom D : Type; 
-```
+axiom D : Type;

tests/positive/MarkdownImport/C.juvix.md

@@ -1,15 +1,7 @@
-# This is a Juvix code block
-
-```juvix
 module C;
 
 import B open;
 
 axiom aa : D;
-```
-
-Text in between code blocks
 
-```juvix
 axiom b : D;
-```

tests/positive/Termination/Data/List.juvix

@@ -11,13 +11,11 @@ type List (A : Type) :=
   | cons : A → List A → List A;
 
 -- Do not remove implicit arguments. Useful for testing.
-foldr
-  : {A : Type} → {B : Type} → (A → B → B) → B → List A → B
+foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → B
   | _ z nil := z
   | f z (cons h hs) := f h (foldr {_} f z hs);
 
-foldl
-  : {A : Type} → {B : Type} → (B → A → B) → B → List A → B
+foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B
   | f z nil := z
   | {_} {_} f z (cons h hs) := foldl {_} f (f z h) hs;
 
@@ -27,8 +25,7 @@ map : {A : Type} → {B : Type} → (A → B) → List A → List B
 
 filter : {A : Type} → (A → Bool) → List A → List A
   | f nil := nil
-  | f (cons h hs) :=
-    ite (f h) (cons h (filter {_} f hs)) (filter f hs);
+  | f (cons h hs) := ite (f h) (cons h (filter {_} f hs)) (filter f hs);
 
 length : {A : Type} → List A → ℕ
   | nil := zero

tests/positive/issue1693/M.juvix

@@ -2,14 +2,7 @@ module M;
 
 import Stdlib.Prelude open;
 
-S
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (A → B → C)
-    → (A → B)
-    → A
-    → C
+S : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → (A → B) → A → C
   | x y z := x z (y z);
 
 K : {A : Type} → {B : Type} → A → B → A

tests/positive/issue1731/builtinFail.juvix

@@ -6,7 +6,4 @@ import Stdlib.System.IO open;
 builtin fail
 axiom fail : {A : Type} → String → A;
 
-main : IO :=
-  printStringLn "Get"
-    >>> fail "Enough"
-    >>> printStringLn "Sleep";
+main : IO := printStringLn "Get" >>> fail "Enough" >>> printStringLn "Sleep";

tests/positive/issue3048/Other.juvix

@@ -1,5 +1,7 @@
 module Other;
 
 type T1 := mkT1;
+
 type T2 := mkT2;
+
 type T3 := mkT3;

tests/positive/issue3048/main.juvix

@@ -3,14 +3,6 @@ module main;
 import Other;
 
 type Tree (A : Type) :=
-  node (Tree A)
-       (Tree A)
-       (Tree A)
-       (Tree A)
-       (Tree A)
-       (Tree A)
-       (Tree A)
-       (Tree A)
-       (Tree A);
+  node (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A) (Tree A);
 
 type Foo := mkFoo (Tree Foo);