diff --git a/Package.juvix b/Package.juvix
index f9e5479e..91d77415 100644
--- a/Package.juvix
+++ b/Package.juvix
@@ -3,7 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "stdlib";
-     version := mkVersion 0 0 1;
-     dependencies := []};
+  defaultPackage@?{
+    name := "stdlib";
+    version := mkVersion 0 0 1;
+    dependencies := []
+  };
diff --git a/Stdlib/Cairo/Ec.juvix b/Stdlib/Cairo/Ec.juvix
index 77cd0743..fcf44b71 100644
--- a/Stdlib/Cairo/Ec.juvix
+++ b/Stdlib/Cairo/Ec.juvix
@@ -12,17 +12,13 @@ import Stdlib.Data.Bool open;
 module StarkCurve;
   ALPHA : Field := 1;
 
-  BETA : Field :=
-    0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89;
+  BETA : Field := 0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89;
 
-  ORDER : Field :=
-    0x800000000000010ffffffffffffffffb781126dcae7b2321e66a241adc64d2f;
+  ORDER : Field := 0x800000000000010ffffffffffffffffb781126dcae7b2321e66a241adc64d2f;
 
-  GEN_X : Field :=
-    0x1ef15c18599971b7beced415a40f0c7deacfd9b0d1819e03d723d8bc943cfca;
+  GEN_X : Field := 0x1ef15c18599971b7beced415a40f0c7deacfd9b0d1819e03d723d8bc943cfca;
 
-  GEN_Y : Field :=
-    0x5668060aa49730b7be4801df46ec62de53ecd11abe43a32873000c36e8dc1f;
+  GEN_Y : Field := 0x5668060aa49730b7be4801df46ec62de53ecd11abe43a32873000c36e8dc1f;
 end;
 
 builtin ec_point
@@ -45,8 +41,7 @@ isOnCurve : Point -> Bool
   | (mkPoint x y) :=
     if
       | y == 0 := x == 0
-      | else :=
-        y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
+      | 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
@@ -58,7 +53,10 @@ double : Point -> Point
           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);
+        in mkPoint@?{
+          x := r_x;
+          y := r_y
+        };
 
 --- Adds two valid points on the EC.
 add : Point -> Point -> Point
@@ -109,8 +107,7 @@ addMul (p : Point) (m : Field) (q : Point) : Point :=
       in sub r s;
 
 --- Computes m * p on the elliptic curve.
-mul (m : Field) (p : Point) : Point :=
-  addMul (mkPoint 0 0) m p;
+mul (m : Field) (p : Point) : Point := addMul (mkPoint 0 0) m p;
 
 module Operators;
   import Stdlib.Data.Fixity open;
diff --git a/Stdlib/Cairo/Poseidon.juvix b/Stdlib/Cairo/Poseidon.juvix
index d9752d18..a025b2eb 100644
--- a/Stdlib/Cairo/Poseidon.juvix
+++ b/Stdlib/Cairo/Poseidon.juvix
@@ -19,13 +19,11 @@ axiom poseidonHash : PoseidonState -> PoseidonState;
 
 --- Hashes one element and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHash1 (x : Field) : Field :=
-  PoseidonState.s0 (poseidonHash (mkPoseidonState x 0 1));
+poseidonHash1 (x : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseidonState x 0 1));
 
 --- Hashes two elements and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHash2 (x y : Field) : Field :=
-  PoseidonState.s0 (poseidonHash (mkPoseidonState x y 2));
+poseidonHash2 (x y : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseidonState x y 2));
 
 --- Hashes n elements and retrieves a single field element output.
 {-# eval: false #-}
@@ -33,18 +31,7 @@ poseidonHashList (lst : List Field) : Field :=
   let
     go (acc : PoseidonState) : List Field -> PoseidonState
       | [] := poseidonHash acc@PoseidonState{s0 := s0 + 1}
-      | [x] :=
-        poseidonHash
-          acc@PoseidonState{
-            s0 := s0 + x;
-            s1 := s1 + 1
-          }
+      | [x] := poseidonHash acc@PoseidonState{   s0 := s0 + x; s1 := s1 + 1 }
       | (x1 :: x2 :: xs) :=
-        go
-          (poseidonHash
-            acc@PoseidonState{
-              s0 := s0 + x1;
-              s1 := s1 + x2
-            })
-          xs;
+        go (poseidonHash acc@PoseidonState{   s0 := s0 + x1; s1 := s1 + x2 }) xs;
   in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst);
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index 956b5279..57724709 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/Stdlib/Data/List/Base.juvix
@@ -67,12 +67,10 @@ filter {A} (f : A → Bool) : List A → List A
   | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs);
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
-length {A} (l : List A) : Nat :=
-  for (acc := zero) (_ in l) {suc acc};
+length {A} (l : List A) : Nat := for (acc := zero) (_ in l) {suc acc};
 
 --- 𝒪(𝓃). Returns the given ;List; in reverse order.
-reverse {A} (l : List A) : List A :=
-  for (acc := nil) (x in l) {x :: acc};
+reverse {A} (l : List A) : List A := for (acc := nil) (x in l) {x :: acc};
 
 --- Returns a ;List; of length n where every element is the given value.
 replicate {A} : Nat → A → List A
@@ -95,8 +93,7 @@ splitAt {A} : Nat → List A → Pair (List A) (List A)
   | _ nil := nil, nil
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
-  | (suc m) (x :: xs) :=
-    case splitAt m xs of l1, l2 := x :: l1, l2;
+  | (suc m) (x :: xs) := case splitAt m xs of l1, l2 := x :: l1, l2;
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
 terminating
@@ -110,12 +107,9 @@ merge {A} {{Ord A}} : List A → List A → List A
 
 --- 𝒪(𝓃). Returns a tuple where the first component has the items that
 --- satisfy the predicate and the second component has the elements that don't.
-partition
-  {A} (f : A → Bool) : List A → Pair (List A) (List A)
+partition {A} (f : A → Bool) : List A → Pair (List A) (List A)
   | nil := nil, nil
-  | (x :: xs) :=
-    case partition f xs of
-      l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2);
+  | (x :: xs) := case partition f xs of l1, l2 := ite (f x) (x :: l1, l2) (l1, x :: l2);
 
 syntax operator ++ cons;
 
@@ -128,8 +122,7 @@ syntax operator ++ cons;
 snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil;
 
 --- Concatenates a ;List; of ;List;s.
-flatten : {A : Type} → List (List A) → List A :=
-  foldl (++) nil;
+flatten : {A : Type} → List (List A) → List A := foldl (++) nil;
 
 --- 𝒪(𝓃). Inserts the given element before every element in the given ;List;.
 prependToAll {A} (sep : A) : List A → List A
@@ -174,8 +167,7 @@ null {A} : List A → Bool
 --- 𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function
 --- to each pair of elements from the input lists.
 {-# specialize: [1] #-}
-zipWith
-  {A B C} (f : A -> B -> C) : List A -> List B -> List C
+zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List C
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
@@ -212,9 +204,7 @@ quickSort {A} {{Ord A}} : List A → List A :=
     go : List A → List A
       | nil := nil
       | xs@(_ :: nil) := xs
-      | (x :: xs) :=
-        case partition (Ord.cmp x >> isGT) xs of
-          l1, l2 := go l1 ++ x :: go l2;
+      | (x :: xs) := case partition (Ord.cmp x >> isGT) xs of l1, l2 := go l1 ++ x :: go l2;
   in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
@@ -227,8 +217,7 @@ syntax iterator concatMap {init := 0; range := 1};
 
 --- Applies a function to every item on a ;List; and concatenates the result.
 --- 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.
-concatMap {A B} (f : A -> List B) : List A -> List B :=
-  map f >> flatten;
+concatMap {A B} (f : A -> List B) : List A -> List B := map f >> flatten;
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : List (List A) -> List (List A)
diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix
index a2b6097a..b3a24088 100644
--- a/Stdlib/Data/Pair.juvix
+++ b/Stdlib/Data/Pair.juvix
@@ -10,8 +10,7 @@ import Stdlib.Trait.Show open;
 
 instance
 eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
-  | {{mkEq eq-a}} {{mkEq eq-b}} :=
-    mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
+  | {{mkEq eq-a}} {{mkEq eq-b}} := mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
 
 instance
 ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
@@ -24,9 +23,6 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
           | EQ := cmp-b b1 b2};
 
 instance
-showProductI
-  {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
+showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
   | {{mkShow show-a}} {{mkShow show-b}} :=
-    mkShow
-      λ {(a, b) :=
-        "(" ++str show-a a ++str " , " ++str show-b b ++str ")"};
+    mkShow λ {(a, b) := "(" ++str show-a a ++str " , " ++str show-b b ++str ")"};
diff --git a/Stdlib/Data/Pair/Base.juvix b/Stdlib/Data/Pair/Base.juvix
index 7d29d9b6..5d1d77c4 100644
--- a/Stdlib/Data/Pair/Base.juvix
+++ b/Stdlib/Data/Pair/Base.juvix
@@ -12,8 +12,7 @@ uncurry {A B C} (f : A -> B -> C) : Pair A B -> C
   | (a, b) := f a b;
 
 --- Converts a function with a product argument to a function of two arguments.
-curry {A B C} (f : Pair A B -> C) (a : A) (b : B) : C :=
-  f (a, b);
+curry {A B C} (f : Pair A B -> C) (a : A) (b : B) : C := f (a, b);
 
 --- Projects the first component of a tuple.
 fst {A B} : Pair A B → A
diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
index 45c0a01f..65f75cb3 100644
--- a/Stdlib/Data/Range.juvix
+++ b/Stdlib/Data/Range.juvix
@@ -18,19 +18,12 @@ type Range N :=
 syntax iterator for {init := 1; range := 1};
 
 {-# specialize: [1, 2, 3, 5] #-}
-for
-  {A N}
-  {{Ord N}}
-  {{Natural N}}
-  (f : A → N → A)
-  (a : A)
-  : Range N → A
+for {A N} {{Ord N}} {{Natural N}} (f : A → N → A) (a : A) : Range N → A
   | mkRange@{low; high; step} :=
     let
       {-# specialize-by: [f] #-}
       terminating
-      go (acc : A) (n : N) : A :=
-        ite (n > high) acc (go (f acc n) (n + step));
+      go (acc : A) (n : N) : A := ite (n > high) acc (go (f acc n) (n + step));
     in go a low;
 
 syntax operator to range;
@@ -43,5 +36,4 @@ syntax operator step step;
 
 --- `x to y step s` is the range [x,x+s,..,y]
 {-# inline: always #-}
-step {N} (r : Range N) (s : N) : Range N :=
-  r@Range{step := s};
+step {N} (r : Range N) (s : N) : Range N := r@Range{step := s};
diff --git a/Stdlib/Data/Result/Base.juvix b/Stdlib/Data/Result/Base.juvix
index 7c1239ca..b0a65c65 100644
--- a/Stdlib/Data/Result/Base.juvix
+++ b/Stdlib/Data/Result/Base.juvix
@@ -12,22 +12,15 @@ type Result E A :=
 
 --- Apply the onError function if the value is ;error; or apply the
 --- onOk function if the value is ;ok;.
-handleResult
-  {E A B}
-  (onError : E -> B)
-  (onOk : A -> B)
-  : Result E A -> B
+handleResult {E A B} (onError : E -> B) (onOk : A -> B) : Result E A -> B
   | (error a) := onError a
   | (ok a) := onOk a;
 
 --- Apply a function to the ;error; value of a Result.
-mapError
-  {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A :=
-  handleResult (f >> error) ok;
+mapError {A E1 E2} (f : E1 -> E2) : Result E1 A -> Result E2 A := handleResult (f >> error) ok;
 
 --- Apply a function to the ;ok; value of a Result.
-mapOk {E A C} (f : A -> C) : Result E A -> Result E C :=
-  handleResult error (f >> ok);
+mapOk {E A C} (f : A -> C) : Result E A -> Result E C := handleResult error (f >> ok);
 
 --- Return ;true; if the value is an ;error;, otherwise ;false;.
 isError {E A} : Result E A -> Bool
@@ -50,11 +43,9 @@ fromOk {E A} (default : A) : Result E A -> A
   | (ok b) := b;
 
 --- Convert a Result to a Maybe. An ;error; value becomes `nothing`.
-resultToMaybe {E A} : Result E A -> Maybe A :=
-  handleResult (const nothing) just;
+resultToMaybe {E A} : Result E A -> Maybe A := handleResult (const nothing) just;
 
 --- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`.
-maybeToResult
-  {E A} (defaultError : E) : Maybe A -> Result E A
+maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A
   | nothing := error defaultError
   | (just x) := ok x;
diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix
index 82a2660e..6c2ecb00 100644
--- a/Stdlib/Data/String/Base.juvix
+++ b/Stdlib/Data/String/Base.juvix
@@ -9,5 +9,4 @@ import Stdlib.Data.Fixity open;
 concatStr : List String -> String := foldl (++str) "";
 
 --- Joins a ;List; of ;String;s with "\n".
-unlines : List String -> String :=
-  intersperse "\n" >> concatStr;
+unlines : List String -> String := intersperse "\n" >> concatStr;
diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix
index 4383431f..5c7455d0 100644
--- a/Stdlib/Extra/Gcd.juvix
+++ b/Stdlib/Extra/Gcd.juvix
@@ -7,14 +7,7 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Data.Bool open;
 
 --- Computes the greatest common divisor.
-gcd
-  {A}
-  {{Eq A}}
-  {{Ord A}}
-  {{Natural A}}
-  {{DivMod A}}
-  (a b : A)
-  : A :=
+gcd {A} {{Eq A}} {{Ord A}} {{Natural A}} {{DivMod A}} (a b : A) : A :=
   let
     -- Internal helper for computing the greatest common divisor. The first element
     -- should be smaller than the second.
diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix
index 21d7fe9d..c1b9e53e 100644
--- a/Stdlib/Function.juvix
+++ b/Stdlib/Function.juvix
@@ -47,8 +47,7 @@ iterate {A} : Nat -> (A -> A) -> A -> A
 syntax operator on lapp;
 
 {-# inline: 2 #-}
-on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C :=
-  f (g a) (g b);
+on {A B C} (f : B → B → C) (g : A → B) (a b : A) : C := f (g a) (g b);
 
 syntax operator >-> seq;
 
diff --git a/Stdlib/System/IO.juvix b/Stdlib/System/IO.juvix
index 36f8c989..63d8871a 100644
--- a/Stdlib/System/IO.juvix
+++ b/Stdlib/System/IO.juvix
@@ -8,8 +8,6 @@ import Stdlib.System.IO.String open public;
 
 import Stdlib.Trait.Show open;
 
-print {A} {{Show A}} (a : A) : IO :=
-  printString (Show.show a);
+print {A} {{Show A}} (a : A) : IO := printString (Show.show a);
 
-printLn {A} {{Show A}} (a : A) : IO :=
-  printStringLn (Show.show a);
+printLn {A} {{Show A}} (a : A) : IO := printStringLn (Show.show a);
diff --git a/Stdlib/System/IO/Bool.juvix b/Stdlib/System/IO/Bool.juvix
index da364e69..23e53233 100644
--- a/Stdlib/System/IO/Bool.juvix
+++ b/Stdlib/System/IO/Bool.juvix
@@ -7,5 +7,4 @@ import Stdlib.System.IO.String open;
 builtin bool-print
 axiom printBool : Bool → IO;
 
-printBoolLn (b : Bool) : IO :=
-  printBool b >>> printString "\n";
+printBoolLn (b : Bool) : IO := printBool b >>> printString "\n";
diff --git a/Stdlib/System/IO/Int.juvix b/Stdlib/System/IO/Int.juvix
index 6c89adcd..abe531e8 100644
--- a/Stdlib/System/IO/Int.juvix
+++ b/Stdlib/System/IO/Int.juvix
@@ -7,5 +7,4 @@ import Stdlib.System.IO.String open;
 builtin int-print
 axiom printInt : Int → IO;
 
-printIntLn (i : Int) : IO :=
-  printInt i >>> printString "\n";
+printIntLn (i : Int) : IO := printInt i >>> printString "\n";
diff --git a/Stdlib/System/IO/Nat.juvix b/Stdlib/System/IO/Nat.juvix
index 99c54fef..8f787ae6 100644
--- a/Stdlib/System/IO/Nat.juvix
+++ b/Stdlib/System/IO/Nat.juvix
@@ -7,5 +7,4 @@ import Stdlib.System.IO.String open;
 builtin nat-print
 axiom printNat : Nat → IO;
 
-printNatLn (n : Nat) : IO :=
-  printNat n >>> printString "\n";
+printNatLn (n : Nat) : IO := printNat n >>> printString "\n";
diff --git a/Stdlib/System/IO/String.juvix b/Stdlib/System/IO/String.juvix
index 511e7036..e79c8668 100644
--- a/Stdlib/System/IO/String.juvix
+++ b/Stdlib/System/IO/String.juvix
@@ -9,5 +9,4 @@ axiom printString : String → IO;
 builtin IO-readline
 axiom readLn : (String → IO) → IO;
 
-printStringLn (s : String) : IO :=
-  printString s >>> printString "\n";
+printStringLn (s : String) : IO := printString s >>> printString "\n";
diff --git a/Stdlib/Trait/Partial.juvix b/Stdlib/Trait/Partial.juvix
index 977cb59b..cf6beebd 100644
--- a/Stdlib/Trait/Partial.juvix
+++ b/Stdlib/Trait/Partial.juvix
@@ -4,10 +4,8 @@ import Stdlib.Data.String.Base open;
 import Stdlib.Debug.Fail as Debug;
 
 trait
-type Partial :=
-  mkPartial {fail : {A : Type} -> String -> A};
+type Partial := mkPartial {fail : {A : Type} -> String -> A};
 
 open Partial public;
 
-runPartial {A} (f : {{Partial}} -> A) : A :=
-  f {{mkPartial Debug.failwith}};
+runPartial {A} (f : {{Partial}} -> A) : A := f {{mkPartial Debug.failwith}};
diff --git a/test/Package.juvix b/test/Package.juvix
index 3bb3adf2..c298a1fa 100644
--- a/test/Package.juvix
+++ b/test/Package.juvix
@@ -3,11 +3,8 @@ module Package;
 import PackageDescription.V2 open;
 
 package : Package :=
-  defaultPackage
-    {name := "stdlib-test";
-     dependencies := [ path "../"
-                     ; github
-                       "anoma"
-                       "juvix-quickcheck"
-                       "8e5d49682fb0b861fc0a1aed95cfebab03231d85"
-                     ]};
+  defaultPackage@?{
+    name := "stdlib-test";
+    dependencies :=
+      [path "../"; github "anoma" "juvix-quickcheck" "8e5d49682fb0b861fc0a1aed95cfebab03231d85"]
+  };
diff --git a/test/Test.juvix b/test/Test.juvix
index 1571528e..1fa4403f 100644
--- a/test/Test.juvix
+++ b/test/Test.juvix
@@ -18,22 +18,15 @@ prop-reverseReverseIsIdentity : List Int -> Bool
   | xs := eqListInt xs (reverse (reverse xs));
 
 prop-tailLengthOneLess : List Int -> Bool
-  | xs :=
-    null xs
-      || ofNat (length (tail xs)) == intSubNat (length xs) 1;
+  | xs := null xs || ofNat (length (tail xs)) == intSubNat (length xs) 1;
 
 prop-splitAtRecombine : Nat -> List Int -> Bool
-  | n xs :=
-    case splitAt n xs of
-      lhs, rhs := eqListInt xs (lhs ++ rhs);
+  | n xs := case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs);
 
 prop-splitAtLength : Nat -> List Int -> Bool
   | n xs :=
-    case
-      splitAt n (xs ++ replicate (sub n (length xs)) (ofNat 0))
-    of
-      lhs, rhs :=
-        length lhs == n && length rhs == sub (length xs) n;
+    case splitAt n (xs ++ replicate (sub n (length xs)) (ofNat 0)) of
+      lhs, rhs := length lhs == n && length rhs == sub (length xs) n;
 -- Make sure the list has length at least n
 
 prop-mergeSumLengths : List Int -> List Int -> Bool
@@ -42,10 +35,7 @@ prop-mergeSumLengths : List Int -> List Int -> Bool
 prop-partition : List Int -> (Int -> Bool) -> Bool
   | xs p :=
     case partition p xs of
-      lhs, rhs :=
-        all p lhs
-          && not (any p rhs)
-          && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
+      lhs, rhs := all p lhs && not (any p rhs) && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
 
 prop-distributive : Int -> Int -> (Int -> Int) -> Bool
   | a b f := f (a + b) == f a + f b;
@@ -70,9 +60,7 @@ prop-sort : (List Int -> List Int) -> List Int -> Bool
         | nil := true
         | (_ :: nil) := true
         | (x :: y :: xs) := x <= y && isSorted (y :: xs);
-    in length sorted == length xs
-      && eqListInt sorted (sort sorted)
-      && isSorted sorted;
+    in length sorted == length xs && eqListInt sorted (sort sorted) && isSorted sorted;
 
 prop-zip : List Int -> List Int -> Bool
   | xs ys :=
@@ -83,8 +71,7 @@ prop-zip : List Int -> List Int -> Bool
       && eqListInt (take expectedLen xs) (map fst zs)
       && eqListInt (take expectedLen ys) (map snd zs);
 
-prop-zipWith
-  : (Int -> Int -> Int) -> List Int -> List Int -> Bool
+prop-zipWith : (Int -> Int -> Int) -> List Int -> List Int -> Bool
   | f xs ys :=
     let
       zs : List Int := zipWith f xs ys;
@@ -104,8 +91,7 @@ prop-drop : Nat -> List Int -> Bool
   | n xs :=
     let
       drop-n : List Int := drop n xs;
-    in length drop-n <= length xs
-      && eqListInt (drop n (drop n xs)) (drop (2 * n) xs);
+    in length drop-n <= length xs && eqListInt (drop n (drop n xs)) (drop (2 * n) xs);
 
 -- Assumption: The input list represents a rectangular matrix
 prop-transposeMatrixId : List (List Int) -> Bool
@@ -126,20 +112,17 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool
           | _ := null xs;
     in checkTxsRowXsCol && checkXsRowTxsCol;
 
-prop-foundElementSatisfiesPredicate
-  (p : Int -> Bool) (xs : List Int) : Bool :=
+prop-foundElementSatisfiesPredicate (p : Int -> Bool) (xs : List Int) : Bool :=
   case find p xs of
     | just x := p x
     | nothing := true;
 
-prop-nonExistenceImpliesPredicateFalseForAll
-  (p : Int -> Bool) (xs : List Int) : Bool :=
+prop-nonExistenceImpliesPredicateFalseForAll (p : Int -> Bool) (xs : List Int) : Bool :=
   case find p xs of
     | just _ := true
     | nothing := all (x in xs) not (p x);
 
-prop-findConsistentWithSplitAt
-  (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool :=
+prop-findConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool :=
   let
     ys×zs := splitAt n xs;
     ys := fst ys×zs;
@@ -152,8 +135,7 @@ prop-findConsistentWithSplitAt
            | else := false
        | nothing := true;
 
-prop-findWithEmptyList (p : Int -> Bool) : Bool :=
-  find p [] == nothing;
+prop-findWithEmptyList (p : Int -> Bool) : Bool := find p [] == nothing;
 
 prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool :=
   if
@@ -163,15 +145,12 @@ prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool :=
         | just _ := true
         | nothing := false;
 
-prop-findWithAlwaysFalseIsNothing (xs : List Int) : Bool :=
-  find (const false) xs == nothing;
+prop-findWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing;
 
-prop-resultErrorApplication
-  (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
+prop-resultErrorApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
   handleResult f g (error x) == f x;
 
-prop-resultOkApplication
-  (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
+prop-resultOkApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
   handleResult f g (ok x) == g x;
 
 prop-resultIsError : Result Int Bool -> Bool
@@ -182,13 +161,11 @@ prop-resultIsOk : Result Int Bool -> Bool
   | x@(error _) := not (isOk x)
   | x@(ok _) := isOk x;
 
-prop-resultFromErrorDefault
-  (defaultError : Int) : Result Int Bool -> Bool
+prop-resultFromErrorDefault (defaultError : Int) : Result Int Bool -> Bool
   | e@(error x) := fromError defaultError e == x
   | e@(ok _) := fromError defaultError e == defaultError;
 
-prop-resultFromOkDefault
-  (defaultOk : Bool) : Result Int Bool -> Bool
+prop-resultFromOkDefault (defaultOk : Bool) : Result Int Bool -> Bool
   | e@(error _) := fromOk defaultOk e == defaultOk
   | e@(ok x) := fromOk defaultOk e == x;
 
@@ -200,8 +177,7 @@ prop-maybeToResult (def : Int) : Maybe Bool -> Bool
   | m@(just x) := maybeToResult def m == ok x
   | m@nothing := maybeToResult def m == error def;
 
-prop-resultMapError
-  (f : Int -> Int) : Result Int Int -> Bool
+prop-resultMapError (f : Int -> Int) : Result Int Int -> Bool
   | e@(error x) := mapError f e == error (f x)
   | e@(ok _) := mapError f e == e;
 
@@ -210,10 +186,7 @@ prop-resultMapOk (f : Int -> Int) : Result Int Int -> Bool
   | e@(ok x) := mapOk f e == ok (f x);
 
 sortTest : String -> (List Int -> List Int) -> QC.Test
-  | sortName sort :=
-    QC.mkTest
-      ("sort properties: " ++str sortName)
-      (prop-sort sort);
+  | sortName sort := QC.mkTest ("sort properties: " ++str sortName) (prop-sort sort);
 
 dropTest : QC.Test := QC.mkTest "drop properties" prop-drop;
 
@@ -221,41 +194,24 @@ snocTest : QC.Test := QC.mkTest "snoc properties" prop-snoc;
 
 zipTest : QC.Test := QC.mkTest "zip properties" prop-zip;
 
-zipWithTest : QC.Test :=
-  QC.mkTest "zipWith properties" prop-zipWith;
+zipWithTest : QC.Test := QC.mkTest "zipWith properties" prop-zipWith;
 
-equalCompareToEqTest : QC.Test :=
-  QC.mkTest
-    "equal Nats compare to EQ"
-    prop-equal-compare-to-eq;
+equalCompareToEqTest : QC.Test := QC.mkTest "equal Nats compare to EQ" prop-equal-compare-to-eq;
 
-gcdNoCoprimeTest : QC.Test :=
-  QC.mkTest "no integers are coprime" prop-gcd-bad;
+gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" prop-gcd-bad;
 
 partitionTest : QC.Test :=
-  QC.mkTest
-    "partition: recombination of the output equals the input"
-    prop-partition;
+  QC.mkTest "partition: recombination of the output equals the input" prop-partition;
 
-testDistributive : QC.Test :=
-  QC.mkTest
-    "all functions are distributive over +"
-    prop-distributive;
+testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" prop-distributive;
 
-reverseLengthTest : QC.Test :=
-  QC.mkTest
-    "reverse preserves length"
-    prop-reverseDoesNotChangeLength;
+reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
-  QC.mkTest
-    "reverse of reverse is identity"
-    prop-reverseReverseIsIdentity;
+  QC.mkTest "reverse of reverse is identity" prop-reverseReverseIsIdentity;
 
 splitAtRecombineTest : QC.Test :=
-  QC.mkTest
-    "splitAt: recombination of the output is equal to the input list"
-    prop-splitAtRecombine;
+  QC.mkTest "splitAt: recombination of the output is equal to the input list" prop-splitAtRecombine;
 
 splitAtLengthTest : QC.Test :=
   QC.mkTest
@@ -268,9 +224,7 @@ mergeSumLengthsTest : QC.Test :=
     prop-mergeSumLengths;
 
 tailLengthOneLessTest : QC.Test :=
-  QC.mkTest
-    "tail: length of output is one less than input unless empty"
-    prop-tailLengthOneLess;
+  QC.mkTest "tail: length of output is one less than input unless empty" prop-tailLengthOneLess;
 
 transposeMatrixIdTest : QC.Test :=
   QC.mkTest
@@ -285,9 +239,7 @@ transposeMatrixDimentionsTest : QC.Test :=
     prop-transposeMatrixDimensions;
 
 findFoundElementSatisfiesPredicate : QC.Test :=
-  QC.mkTest
-    "find: found element satisfies predicate"
-    prop-foundElementSatisfiesPredicate;
+  QC.mkTest "find: found element satisfies predicate" prop-foundElementSatisfiesPredicate;
 
 findNonExistenceImpliesPredicateFalseForAll : QC.Test :=
   QC.mkTest
@@ -295,64 +247,38 @@ findNonExistenceImpliesPredicateFalseForAll : QC.Test :=
     prop-nonExistenceImpliesPredicateFalseForAll;
 
 findConsistentWithSplitAt : QC.Test :=
-  QC.mkTest
-    "find: consistent with splitAt"
-    prop-findConsistentWithSplitAt;
+  QC.mkTest "find: consistent with splitAt" prop-findConsistentWithSplitAt;
 
 findOnEmptyListIsNothing : QC.Test :=
-  QC.mkTest
-    "find: called with empty list is nothing"
-    prop-findWithEmptyList;
+  QC.mkTest "find: called with empty list is nothing" prop-findWithEmptyList;
 
 findWithAlwaysTrueIsJust : QC.Test :=
-  QC.mkTest
-    "find: always true predicate returns just"
-    prop-findWithAlwaysTrueIsJust;
+  QC.mkTest "find: always true predicate returns just" prop-findWithAlwaysTrueIsJust;
 
 findWithAlwaysFalseIsNothing : QC.Test :=
-  QC.mkTest
-    "find: always false predicate returns nothing"
-    prop-findWithAlwaysFalseIsNothing;
+  QC.mkTest "find: always false predicate returns nothing" prop-findWithAlwaysFalseIsNothing;
 
 resultResultErrorApplication : QC.Test :=
-  QC.mkTest
-    "result: result error application"
-    prop-resultErrorApplication;
+  QC.mkTest "result: result error application" prop-resultErrorApplication;
 
 resultResultOkApplication : QC.Test :=
-  QC.mkTest
-    "result: result ok application"
-    prop-resultOkApplication;
+  QC.mkTest "result: result ok application" prop-resultOkApplication;
 
-resultIsError : QC.Test :=
-  QC.mkTest
-    "result: isError detects error"
-    prop-resultIsError;
+resultIsError : QC.Test := QC.mkTest "result: isError detects error" prop-resultIsError;
 
-resultIsOk : QC.Test :=
-  QC.mkTest "result: isOk detects ok" prop-resultIsOk;
+resultIsOk : QC.Test := QC.mkTest "result: isOk detects ok" prop-resultIsOk;
 
-resultFromError : QC.Test :=
-  QC.mkTest
-    "result: fromError uses default"
-    prop-resultFromErrorDefault;
+resultFromError : QC.Test := QC.mkTest "result: fromError uses default" prop-resultFromErrorDefault;
 
-resultFromOk : QC.Test :=
-  QC.mkTest
-    "result: fromOk uses default"
-    prop-resultFromOkDefault;
+resultFromOk : QC.Test := QC.mkTest "result: fromOk uses default" prop-resultFromOkDefault;
 
-resultResultToMaybe : QC.Test :=
-  QC.mkTest "result: resultToMaybe" prop-resultToMaybe;
+resultResultToMaybe : QC.Test := QC.mkTest "result: resultToMaybe" prop-resultToMaybe;
 
-resultMaybeToResult : QC.Test :=
-  QC.mkTest "result: maybeToResult" prop-maybeToResult;
+resultMaybeToResult : QC.Test := QC.mkTest "result: maybeToResult" prop-maybeToResult;
 
-resultMapError : QC.Test :=
-  QC.mkTest "result: mapError" prop-resultMapError;
+resultMapError : QC.Test := QC.mkTest "result: mapError" prop-resultMapError;
 
-resultMapOk : QC.Test :=
-  QC.mkTest "result: mapOk" prop-resultMapOk;
+resultMapOk : QC.Test := QC.mkTest "result: mapOk" prop-resultMapOk;
 
 main : IO :=
   readLn
diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix
index ab94d7d3..6d14a639 100644
--- a/test/Test/Arb.juvix
+++ b/test/Test/Arb.juvix
@@ -6,8 +6,7 @@ import Test.QuickCheck.Arbitrary open;
 import Test.QuickCheck.Gen open;
 import Data.Random open;
 
-arbitrarySizedList
-  {A} (size : Nat) : Arbitrary A -> Arbitrary (List A)
+arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A)
   | (mkArbitrary g) :=
     mkArbitrary
       (mkGen
@@ -24,8 +23,7 @@ arbitrarySizedList
           in randList rand size});
 
 --- Generate an arbitrary rectangular matrix
-arbitraryMatrix
-  {A} {{arbA : Arbitrary A}} : Arbitrary (List (List A)) :=
+arbitraryMatrix {A} {{arbA : Arbitrary A}} : Arbitrary (List (List A)) :=
   mkArbitrary
     (mkGen
       \ {rand :=
diff --git a/test/Test/StdlibTestExtra.juvix b/test/Test/StdlibTestExtra.juvix
index b658101a..5f251ae2 100644
--- a/test/Test/StdlibTestExtra.juvix
+++ b/test/Test/StdlibTestExtra.juvix
@@ -3,8 +3,7 @@ module Test.StdlibTestExtra;
 import Stdlib.Prelude open;
 
 instance
-eitherShow
-  {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
+eitherShow {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
   mkShow@{
     show : Result A B -> String
       | (error x) := "Error (" ++str Show.show x ++str ")"
diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml
index fb83cc54..aa5b5da8 100644
--- a/test/juvix.lock.yaml
+++ b/test/juvix.lock.yaml
@@ -2,7 +2,7 @@
 # Do not edit this file manually.
 
 version: 2
-checksum: 8013d01c2b6d46596d97438913b23987618efe1f7a6e54e7abd22dd5e0ae7f43
+checksum: 6ad1c42b98c3512560e5de4a3502d387b92fe6ea883f40a59299d10f17bd3851
 dependencies:
 - path: ../
   dependencies: []