diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix
index 498e44c7..d91be1f3 100644
--- a/Stdlib/Data/Bool/Base.juvix
+++ b/Stdlib/Data/Bool/Base.juvix
@@ -36,9 +36,7 @@ if : {A : Type} → Bool → A → A → A
   | false _ b := b;
 
 --- Logical disjunction.
-or : Bool → Bool → Bool
-  | a b := a || b;
+or (a b : Bool) : Bool := a || b;
 
 --- Logical conjunction.
-and : Bool → Bool → Bool
-  | a b := a && b;
+and (a b : Bool) : Bool := a && b;
diff --git a/Stdlib/Data/Int/Base.juvix b/Stdlib/Data/Int/Base.juvix
index 55ea644f..c5010ce0 100644
--- a/Stdlib/Data/Int/Base.juvix
+++ b/Stdlib/Data/Int/Base.juvix
@@ -27,11 +27,10 @@ nonNeg : Int -> Bool
 
 --- Subtraction for ;Nat;s.
 builtin int-sub-nat
-intSubNat : Nat -> Nat -> Int
-  | m n :=
-    case sub n m
-      | zero := ofNat (Nat.sub m n)
-      | suc k := negSuc k;
+intSubNat (n m : Nat) : Int :=
+  case sub n m
+    | zero := ofNat (Nat.sub m n)
+    | suc k := negSuc k;
 
 syntax operator + additive;
 
@@ -69,8 +68,7 @@ syntax operator - additive;
 
 --- Subtraction for ;Int;s.
 builtin int-sub
-- : Int -> Int -> Int
-  | m n := m + neg n;
+- (n m : Int) : Int := m + neg n;
 
 --- Division for ;Int;s.
 builtin int-div
diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix
index 9cae1e95..b1918ad3 100644
--- a/Stdlib/Data/Int/Ord.juvix
+++ b/Stdlib/Data/Int/Ord.juvix
@@ -20,43 +20,36 @@ builtin int-eq
 syntax operator /= comparison;
 
 --- Tests for inequality.
-/= : Int -> Int -> Bool
-  | m n := not (m == n);
+/= (m n : Int) : Bool := not (m == n);
 
 syntax operator <= comparison;
 
 --- Returns ;true; iff the first element is less than or equal to the second.
 builtin int-le
-<= : Int -> Int -> Bool
-  | m n := nonNeg (n - m);
+<= (m n : Int) : Bool := nonNeg (n - m);
 
 syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
 builtin int-lt
-< : Int -> Int -> Bool
-  | m n := m + 1 <= n;
+< (m n : Int) : Bool := m + 1 <= n;
 
 syntax operator > comparison;
 
 --- Returns ;true; iff the first element is greater than the second.
-> : Int -> Int -> Bool
-  | m n := n < m;
+> (m n : Int) : Bool := n < m;
 
 syntax operator >= comparison;
 
 --- Returns ;true; iff the first element is greater than or equal to the second.
->= : Int -> Int -> Bool
-  | m n := n <= m;
+>= (m n : Int) : Bool := n <= m;
 
 --- Tests for ;Ordering;.
-compare : Int -> Int -> Ordering
-  | m n := if (m == n) EQ (if (m < n) LT GT);
+compare (m n : Int) : Ordering :=
+  if (m == n) EQ (if (m < n) LT GT);
 
 --- Returns the smallest ;Int;.
-min : Int → Int → Int
-  | x y := if (x < y) x y;
+min (x y : Int) : Int := if (x < y) x y;
 
 --- Returns the biggest ;Int;.
-max : Int → Int → Int
-  | x y := if (x > y) x y;
+max (x y : Int) : Int := if (x > y) x y;
diff --git a/Stdlib/Data/Int/Range.juvix b/Stdlib/Data/Int/Range.juvix
index d48a7d00..fb5244e7 100644
--- a/Stdlib/Data/Int/Range.juvix
+++ b/Stdlib/Data/Int/Range.juvix
@@ -17,20 +17,18 @@ type Range :=
 syntax iterator for {init: 1, range: 1};
 
 {-# specialize: [1, 3] #-}
-for : {A : Type} → (A → Int → A) → A → Range → A
-  | {A} f a mkRange@{low; high; step} :=
+for {A} (f : A → Int → A) (a : A) : Range → A
+  | mkRange@{low; high; step} :=
     let
       terminating
-      go : A → Int → A;
-      go acc n := if (n > high) acc (go (f acc n) (n + step));
+      go (acc : A) (n : Int) : A :=
+        if (n > high) acc (go (f acc n) (n + step));
     in go a low;
 
 syntax operator to range;
 
-to : Int → Int → Range
-  | l h := mkRange l h 1;
+to (l h : Int) : Range := mkRange l h 1;
 
 syntax operator step step;
 
-step : Range → Int → Range
-  | r s := r @Range{step := s};
+step (r : Range) (s : Int) : Range := r@Range{step := s};
diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
index 07f4994f..87488281 100644
--- a/Stdlib/Data/List.juvix
+++ b/Stdlib/Data/List.juvix
@@ -15,41 +15,41 @@ import Stdlib.Trait.Show as Show;
 open Show using {Show};
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
-head : {A : Type} → List A → A
+head {A} : List A → A
   | (x :: _) := x
   | nil := fail "head: empty list";
 
 module ListTraits;
-  Eq : {A : Type} -> Eq.Eq A -> Eq.Eq (List A)
-    | {A} (Eq.mkEq eq-a) :=
+  Eq {A} : Eq.Eq A -> Eq.Eq (List A)
+    | (Eq.mkEq eq-a) :=
       let
-        go : List A -> List A -> Bool;
-        go nil nil := true;
-        go nil _ := false;
-        go _ nil := false;
-        go (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
+        go : List A -> List A -> Bool
+          | nil nil := true
+          | nil _ := false
+          | _ nil := false
+          | (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
       in Eq.mkEq go;
 
-  Ord : {A : Type} -> Ord.Ord A -> Ord.Ord (List A)
-    | {A} (Ord.mkOrd cmp-a) :=
+  Ord {A} : Ord.Ord A -> Ord.Ord (List A)
+    | (Ord.mkOrd cmp-a) :=
       let
-        go : List A -> List A -> Ord.Ordering;
-        go nil nil := Ord.EQ;
-        go nil _ := Ord.LT;
-        go _ nil := Ord.GT;
-        go (x :: xs) (y :: ys) :=
-          case cmp-a x y
-            | Ord.LT := Ord.LT
-            | Ord.GT := Ord.GT
-            | Ord.EQ := go xs ys;
+        go : List A -> List A -> Ord.Ordering
+          | nil nil := Ord.EQ
+          | nil _ := Ord.LT
+          | _ nil := Ord.GT
+          | (x :: xs) (y :: ys) :=
+            case cmp-a x y
+              | Ord.LT := Ord.LT
+              | Ord.GT := Ord.GT
+              | Ord.EQ := go xs ys;
       in Ord.mkOrd go;
 
-  Show : {A : Type} -> Show.Show A -> Show.Show (List A)
-    | {A} (Show.mkShow to-str) :=
+  Show {A} : Show.Show A -> Show.Show (List A)
+    | (Show.mkShow to-str) :=
       let
-        go : List A -> String;
-        go nil := "nil";
-        go (x :: xs) := to-str x ++str " :: " ++str go xs;
+        go : List A -> String
+          | nil := "nil"
+          | (x :: xs) := to-str x ++str " :: " ++str go xs;
       in Show.mkShow
         λ {
           | nil := "nil"
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index f545202c..068ae41d 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/Stdlib/Data/List/Base.juvix
@@ -22,28 +22,28 @@ type List (a : Type) :=
 --- 𝒪(𝓃). Returns ;true; if the given
 --- object is in the ;List;.
 {-# specialize: [1] #-}
-elem : {A : Type} → (A → A → Bool) → A → List A → Bool
-  | _ _ nil := false
-  | eq s (x :: xs) := eq s x || elem eq s xs;
+elem {A} (eq : A → A → Bool) (s : A) : List A → Bool
+  | nil := false
+  | (x :: xs) := eq s x || elem eq s xs;
 
 --- Right-associative fold.
 {-# specialize: [1] #-}
-foldr : {A B : Type} → (A → B → B) → B → List A → B
-  | _ z nil := z
-  | f z (h :: hs) := f h (foldr f z hs);
+foldr {A B} (f : A → B → B) (z : B) : List A → B
+  | nil := z
+  | (h :: hs) := f h (foldr f z hs);
 
 syntax iterator rfor {init: 1, range: 1};
 
 {-# specialize: [1] #-}
-rfor : {A B : Type} → (B → A → B) → B → List A → B
-  | _ acc nil := acc
-  | f acc (x :: xs) := f (rfor f acc xs) x;
+rfor {A B} (f : B → A → B) (acc : B) : List A → B
+  | nil := acc
+  | (x :: xs) := f (rfor f acc xs) x;
 
 --- Left-associative and tail-recursive fold.
 {-# specialize: [1] #-}
-foldl : {A B : Type} → (B → A → B) → B → List A → B
-  | f z nil := z
-  | f z (h :: hs) := foldl f (f z h) hs;
+foldl {A B} (f : B → A → B) (z : B) : List A → B
+  | nil := z
+  | (h :: hs) := foldl f (f z h) hs;
 
 syntax iterator for {init: 1, range: 1};
 
@@ -54,45 +54,45 @@ syntax iterator map {init: 0, range: 1};
 
 --- 𝒪(𝓃). Maps a function over each element of a ;List;.
 {-# specialize: [1] #-}
-map : {A B : Type} → (A → B) → List A → List B
-  | f nil := nil
-  | f (h :: hs) := f h :: map f hs;
+map {A B} (f : A → B) : List A → List B
+  | nil := nil
+  | (h :: hs) := f h :: map f hs;
 
 syntax iterator filter {init: 0, range: 1};
 
 --- 𝒪(𝓃). Filters a ;List; according to a given predicate, i.e.,
 --- keeps the elements for which the given predicate returns ;true;.
 {-# specialize: [1] #-}
-filter : {A : Type} → (A → Bool) → List A → List A
-  | _ nil := nil
-  | f (h :: hs) := if (f h) (h :: filter f hs) (filter f hs);
+filter {A} (f : A → Bool) : List A → List A
+  | nil := nil
+  | (h :: hs) := if (f h) (h :: filter f hs) (filter f hs);
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
-length : {A : Type} → List A → Nat
-  | l := for (acc := 0) (_ in l) {acc + 1};
+length {A} (l : List A) : Nat :=
+  for (acc := 0) (_ in l) {acc + 1};
 
 --- 𝒪(𝓃). Returns the given ;List; in reverse order.
-reverse : {A : Type} → List A → List A
-  | l := 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 : Type} → Nat → A → List A
+replicate {A} : Nat → A → List A
   | zero _ := nil
   | (suc n) x := x :: replicate n x;
 
 --- Takes the first n elements of a ;List;.
-take : {A : Type} → Nat → List A → List A
+take {A} : Nat → List A → List A
   | (suc n) (x :: xs) := x :: take n xs
   | _ _ := nil;
 
 --- Drops the first n elements of a ;List;.
-drop : {A : Type} → Nat → List A → List A
+drop {A} : Nat → List A → List A
   | (suc n) (x :: xs) := drop n xs
   | _ xs := xs;
 
 --- 𝒪(𝓃). splitAt n xs returns a tuple where first element is xs
 --- prefix of length n and second element is the remainder of the ;List;.
-splitAt : {A : Type} → Nat → List A → List A × List A
+splitAt {A} : Nat → List A → List A × List A
   | _ nil := nil, nil
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
@@ -101,7 +101,7 @@ splitAt : {A : Type} → Nat → List A → List A × List A
       | l1, l2 := x :: l1, l2;
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
-merge : {A : Type} → Ord A → List A → List A → List A
+merge {A} : Ord A → List A → List A → List A
   | o@(mkOrd cmp) (x :: xs) (y :: ys) :=
     if
       (isLT (cmp x y))
@@ -112,10 +112,9 @@ merge : {A : Type} → 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 : Type} → (A → Bool) → List A → List A × List A
-  | _ nil := nil, nil
-  | f (x :: xs) :=
+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);
 
@@ -127,25 +126,24 @@ syntax operator ++ cons;
   | (x :: xs) ys := x :: xs ++ ys;
 
 --- 𝒪(𝓃). Append an element.
-snoc : {A : Type} -> List A -> A -> List A
-  | xs x := xs ++ x :: nil;
+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;
 
 --- 𝒪(𝓃). Inserts the given element before every element in the given ;List;.
-prependToAll : {A : Type} → A → List A → List A
-  | _ nil := nil
-  | sep (x :: xs) := sep :: x :: prependToAll sep xs;
+prependToAll {A} (sep : A) : List A → List A
+  | nil := nil
+  | (x :: xs) := sep :: x :: prependToAll sep xs;
 
 --- 𝒪(𝓃). Inserts the given element inbetween every two elements in the given ;List;.
-intersperse : {A : Type} → A → List A → List A
-  | _ nil := nil
-  | sep (x :: xs) := x :: prependToAll sep xs;
+intersperse {A} (sep : A) : List A → List A
+  | nil := nil
+  | (x :: xs) := x :: prependToAll sep xs;
 
 --- 𝒪(1). Drops the first element of a ;List;.
-tail : {A : Type} → List A → List A
+tail {A} : List A → List A
   | (_ :: xs) := xs
   | nil := nil;
 
@@ -153,77 +151,72 @@ syntax iterator any {init: 0, range: 1};
 
 --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.
 {-# specialize: [1] #-}
-any : {A : Type} → (A → Bool) → List A → Bool
-  | f nil := false
-  | f (x :: xs) := if (f x) true (any f xs);
+any {A} (f : A → Bool) : List A → Bool
+  | nil := false
+  | (x :: xs) := if (f x) true (any f xs);
 
 syntax iterator all {init: 0, range: 1};
 
 --- 𝒪(𝓃). Returns ;true; if all elements of the ;List; satisfy the predicate.
 {-# specialize: [1] #-}
-all : {A : Type} -> (A -> Bool) -> List A -> Bool
-  | f nil := true
-  | f (x :: xs) := if (f x) (all f xs) false;
+all {A} (f : A -> Bool) : List A -> Bool
+  | nil := true
+  | (x :: xs) := if (f x) (all f xs) false;
 
 --- 𝒪(1). Returns ;true; if the ;List; is empty.
-null : {A : Type} → List A → Bool
+null {A} : List A → Bool
   | nil := true
   | _ := false;
 
 --- 𝒪(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 : Type}
-    -> (A -> B -> C)
-    -> List A
-    -> List B
-    -> List C
-  | f nil _ := nil
-  | f _ nil := nil
-  | f (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
+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;
 
 --- 𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists.
-zip : {A B : Type} -> List A -> List B -> List (A × B)
+zip {A B} : List A -> List B -> List (A × B)
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := (x, y) :: zip xs ys;
 
 --- 𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort
 --- algorithm.
-mergeSort : {A : Type} → Ord A → List A → List A
-  | {A} o l :=
-    let
-      terminating
-      go : Nat -> List A -> List A;
-      go zero _ := nil;
-      go (suc zero) xs := xs;
-      go len xs :=
+mergeSort {A} (o : Ord A) (l : List A) : List A :=
+  let
+    terminating
+    go : Nat -> List A -> List A
+      | zero _ := nil
+      | (suc zero) xs := xs
+      | len xs :=
         let
           len' : Nat := div len 2;
           splitXs : List A × List A := splitAt len' xs;
           left : List A := fst splitXs;
           right : List A := snd splitXs;
         in merge o (go len' left) (go (sub len len') right);
-    in go (length l) l;
+  in go (length l) l;
 
 --- On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in
 --- ascending order using the QuickSort algorithm.
 terminating
-quickSort : {A : Type} → Ord A → List A → List A
-  | {A} (mkOrd cmp) :=
+quickSort {A} : Ord A → List A → List A
+  | (mkOrd cmp) :=
     let
       terminating
-      go : List A → List A;
-      go nil := nil;
-      go xs@(_ :: nil) := xs;
-      go (x :: xs) :=
-        case partition (isGT ∘ cmp x) xs
-          | l1, l2 := go l1 ++ x :: go l2;
+      go : List A → List A
+        | nil := nil
+        | xs@(_ :: nil) := xs
+        | (x :: xs) :=
+          case partition (isGT ∘ cmp x) xs
+            | l1, l2 := go l1 ++ x :: go l2;
     in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
-catMaybes : {A : Type} -> List (Maybe A) -> List A
+catMaybes {A} : List (Maybe A) -> List A
   | nil := nil
   | (just h :: hs) := h :: catMaybes hs
   | (nothing :: hs) := catMaybes hs;
@@ -232,12 +225,11 @@ 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 : Type} -> (A -> List B) -> List A -> List B
-  | f := flatten ∘ map f;
+concatMap {A B} (f : A -> List B) : List A -> List B :=
+  flatten ∘ map f;
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
-transpose : {A : Type} -> List (List A) -> List (List A)
+transpose {A} : List (List A) -> List (List A)
   | nil := nil
   | (xs :: nil) := map λ {x := x :: nil} xs
   | (xs :: xss) := zipWith (::) xs (transpose xss);
diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
index 4ed106e1..03d72c4d 100644
--- a/Stdlib/Data/Maybe.juvix
+++ b/Stdlib/Data/Maybe.juvix
@@ -15,7 +15,7 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
 
 module MaybeTraits;
-  Eq : {A : Type} -> Eq.Eq A -> Eq.Eq (Maybe A)
+  Eq {A} : Eq.Eq A -> Eq.Eq (Maybe A)
     | (Eq.mkEq eq) :=
       Eq.mkEq
         λ {
@@ -24,7 +24,7 @@ module MaybeTraits;
           | _ _ := false
         };
 
-  Show : {A : Type} -> Show.Show A -> Show.Show (Maybe A)
+  Show {A} : Show.Show A -> Show.Show (Maybe A)
     | (Show.mkShow show) :=
       Show.mkShow
         λ {
@@ -32,7 +32,7 @@ module MaybeTraits;
           | (just a) := "just " ++str show a
         };
 
-  Ord : {A : Type} -> Ord.Ord A -> Ord.Ord (Maybe A)
+  Ord {A} : Ord.Ord A -> Ord.Ord (Maybe A)
     | (Ord.mkOrd cmp) :=
       Ord.mkOrd
         λ {
diff --git a/Stdlib/Data/Maybe/Base.juvix b/Stdlib/Data/Maybe/Base.juvix
index db6b3765..cce7c603 100644
--- a/Stdlib/Data/Maybe/Base.juvix
+++ b/Stdlib/Data/Maybe/Base.juvix
@@ -2,19 +2,19 @@ module Stdlib.Data.Maybe.Base;
 
 --- Represents an optional value that may or may not be present. Provides a way
 --- to handle null or missing values in a type-safe manner.
-type Maybe (A : Type) :=
+type Maybe A :=
   | nothing
   | just A;
 
 --- Extracts the value from a ;Maybe; if present, else returns the given value.
 {-# inline: true #-}
-fromMaybe : {A : Type} → A → Maybe A → A
-  | a nothing := a
-  | _ (just a) := a;
+fromMaybe {A} (a : A) : Maybe A → A
+  | nothing := a
+  | (just a) := a;
 
 --- Applies a function to the value from a ;Maybe; if present, else returns the
 --- given value.
 {-# inline: true #-}
-maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B
-  | b _ nothing := b
-  | _ f (just a) := f a;
+maybe {A B} (b : B) (f : A → B) : Maybe A → B
+  | nothing := b
+  | (just a) := f a;
diff --git a/Stdlib/Data/Nat/Base.juvix b/Stdlib/Data/Nat/Base.juvix
index 60ea93be..8f5d56b6 100644
--- a/Stdlib/Data/Nat/Base.juvix
+++ b/Stdlib/Data/Nat/Base.juvix
@@ -40,10 +40,8 @@ udiv : Nat → Nat → Nat
 
 --- Division for ;Nat;s.
 builtin nat-div
-div : Nat → Nat → Nat
-  | n m := udiv (sub (suc n) m) m;
+div (n m : Nat) : Nat := udiv (sub (suc n) m) m;
 
 --- Modulo for ;Nat;s.
 builtin nat-mod
-mod : Nat → Nat → Nat
-  | n m := sub n (div n m * m);
+mod (n m : Nat) : Nat := sub n (div n m * m);
diff --git a/Stdlib/Data/Nat/Gcd.juvix b/Stdlib/Data/Nat/Gcd.juvix
index ae33ad89..f2065834 100644
--- a/Stdlib/Data/Nat/Gcd.juvix
+++ b/Stdlib/Data/Nat/Gcd.juvix
@@ -4,12 +4,11 @@ import Stdlib.Data.Nat open;
 import Stdlib.Data.Bool open;
 import Stdlib.Data.Nat.Ord open;
 
---- Internal helper for computing the greatest common divisor. The first element
---- should be smaller than the second.
-terminating
-gcd' : Nat → Nat → Nat
-  | a b := if (a == 0) b (gcd' (mod b a) a);
-
 --- Computes the greatest common divisor.
-gcd : Nat → Nat → Nat
-  | a b := if (a > b) (gcd' b a) (gcd' a b);
+gcd (a b : Nat) : Nat :=
+  let
+    -- Internal helper for computing the greatest common divisor. The first element
+    -- should be smaller than the second.
+    terminating
+    gcd' (a b : Nat) : Nat := if (a == 0) b (gcd' (mod b a) a);
+  in if (a > b) (gcd' b a) (gcd' a b);
diff --git a/Stdlib/Data/Nat/Ord.juvix b/Stdlib/Data/Nat/Ord.juvix
index f31c4f26..2f611be9 100644
--- a/Stdlib/Data/Nat/Ord.juvix
+++ b/Stdlib/Data/Nat/Ord.juvix
@@ -19,8 +19,7 @@ builtin nat-eq
 syntax operator /= comparison;
 
 --- Tests for inequality.
-/= : Nat → Nat → Bool
-  | x y := not (x == y);
+/= (x y : Nat) : Bool := not (x == y);
 
 syntax operator <= comparison;
 
@@ -35,29 +34,24 @@ syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
 builtin nat-lt
-< : Nat → Nat → Bool
-  | n m := suc n <= m;
+< (n m : Nat) : Bool := suc n <= m;
 
 syntax operator > comparison;
 
 --- Returns ;true; iff the first element is greater than the second.
-> : Nat → Nat → Bool
-  | n m := m < n;
+> (n m : Nat) : Bool := m < n;
 
 syntax operator >= comparison;
 
 --- Returns ;true; iff the first element is greater than or equal to the second.
->= : Nat → Nat → Bool
-  | n m := m <= n;
+>= (n m : Nat) : Bool := m <= n;
 
 --- Tests for ;Ordering;.
-compare : Nat → Nat → Ordering
-  | n m := if (n == m) EQ (if (n < m) LT GT);
+compare (n m : Nat) : Ordering :=
+  if (n == m) EQ (if (n < m) LT GT);
 
 --- Returns the smallest ;Nat;.
-min : Nat → Nat → Nat
-  | x y := if (x < y) x y;
+min (x y : Nat) : Nat := if (x < y) x y;
 
 --- Returns the biggest ;Nat;.
-max : Nat → Nat → Nat
-  | x y := if (x > y) x y;
+max (x y : Nat) : Nat := if (x > y) x y;
diff --git a/Stdlib/Data/Nat/Range.juvix b/Stdlib/Data/Nat/Range.juvix
index 3fa86faa..3117d2a4 100644
--- a/Stdlib/Data/Nat/Range.juvix
+++ b/Stdlib/Data/Nat/Range.juvix
@@ -17,22 +17,20 @@ type Range :=
 syntax iterator for {init: 1, range: 1};
 
 {-# specialize: [1, 3] #-}
-for : {A : Type} → (A → Nat → A) → A → Range → A
-  | {A} f a mkRange@{low; high; step} :=
+for {A} (f : A → Nat → A) (a : A) : Range → A
+  | mkRange@{low; high; step} :=
     let
       terminating
-      go : A → Nat → A;
-      go acc n := if (n > high) acc (go (f acc n) (n + step));
+      go (acc : A) (n : Nat) : A :=
+        if (n > high) acc (go (f acc n) (n + step));
     in go a low;
 
 syntax operator to range;
 
 --- `x to y` is the range [x..y]
-to : Nat → Nat → Range
-  | l h := mkRange l h 1;
+to (l h : Nat) : Range := mkRange l h 1;
 
 syntax operator step step;
 
 --- `x to y step s` is the range [x,x+s,..,y]
-step : Range → Nat → Range
-  | r s := r @Range{step := s};
+step (r : Range) (s : Nat) : Range := r@Range{step := s};
diff --git a/Stdlib/Data/Product.juvix b/Stdlib/Data/Product.juvix
index b5dec6f9..6eda4d4e 100644
--- a/Stdlib/Data/Product.juvix
+++ b/Stdlib/Data/Product.juvix
@@ -14,15 +14,11 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
 
 module ProductTraits;
-  Eq : {A B : Type} -> Eq.Eq A -> Eq.Eq B -> Eq.Eq (A × B)
+  Eq {A B} : Eq.Eq A -> Eq.Eq B -> Eq.Eq (A × B)
     | (Eq.mkEq eq-a) (Eq.mkEq eq-b) :=
       Eq.mkEq λ {(a1, b1) (a2, b2) := eq-a a1 a2 && eq-b b1 b2};
 
-  Ord
-    : {A B : Type}
-      -> Ord.Ord A
-      -> Ord.Ord B
-      -> Ord.Ord (A × B)
+  Ord {A B} : Ord.Ord A -> Ord.Ord B -> Ord.Ord (A × B)
     | (Ord.mkOrd cmp-a) (Ord.mkOrd cmp-b) :=
       Ord.mkOrd
         λ {(a1, b1) (a2, b2) :=
@@ -31,11 +27,7 @@ module ProductTraits;
             | Ord.GT := Ord.GT
             | Ord.EQ := cmp-b b1 b2};
 
-  Show
-    : {A B : Type}
-      -> Show.Show A
-      -> Show.Show B
-      -> Show.Show (A × B)
+  Show {A B} : Show.Show A -> Show.Show B -> Show.Show (A × B)
     | (Show.mkShow show-a) (Show.mkShow show-b) :=
       Show.mkShow
         λ {(a, b) :=
diff --git a/Stdlib/Data/Product/Base.juvix b/Stdlib/Data/Product/Base.juvix
index 4b009f31..3a805f5d 100644
--- a/Stdlib/Data/Product/Base.juvix
+++ b/Stdlib/Data/Product/Base.juvix
@@ -6,62 +6,37 @@ syntax operator × functor;
 syntax operator , pair;
 
 --- Inductive pair. I.e. a tuple with two components.
-type × (A : Type) (B : Type) :=
-  | , 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 : Type}
-    -> {B : Type}
-    -> {C : Type}
-    -> (A -> B -> C)
-    -> A × B
-    -> C
-  | f (a, b) := f a b;
+uncurry {A B C} (f : A -> B -> C) : A × B -> C
+  | (a, b) := f a b;
 
 --- Converts a function with a product argument to a function of two arguments.
-curry
-  : {A : Type}
-    -> {B : Type}
-    -> {C : Type}
-    -> (A × B -> C)
-    -> A
-    -> B
-    -> C
-  | f a b := f (a, b);
+curry {A B C} (f : A × B -> C) (a : A) (b : B) : C :=
+  f (a, b);
 
 --- Projects the first component of a tuple.
-fst : {A : Type} → {B : Type} → A × B → A
+fst {A B} : A × B → A
   | (a, _) := a;
 
 --- Projects the second component of a tuple.
-snd : {A : Type} → {B : Type} → A × B → B
+snd {A B} : A × B → B
   | (_, b) := b;
 
 --- Swaps the components of a tuple.
-swap : {A : Type} → {B : Type} → A × B → B × A
+swap {A B} : A × B → B × A
   | (a, b) := b, a;
 
 --- Applies a function to the first component.
-first
-  : {A : Type}
-    → {B : Type}
-    → {A' : Type}
-    → (A → A')
-    → A × B
-    → A' × B
-  | f (a, b) := f a, b;
+first {A B A'} (f : A → A') : A × B → A' × B
+  | (a, b) := f a, b;
 
 --- Applies a function to the second component.
-second
-  : {A : Type}
-    → {B : Type}
-    → {B' : Type}
-    → (B → B')
-    → A × B
-    → A × B'
-  | f (a, b) := a, f b;
+second {A B B'} (f : B → B') : A × B → A × B'
+  | (a, b) := a, f b;
 
 --- Applies a function to both components.
-both : {A : Type} → {B : Type} → (A → B) → A × A → B × B
-  | f (a, b) := f a, f b;
+both {A B} (f : A → B) : A × A → B × B
+  | (a, b) := f a, f b;
diff --git a/Stdlib/Data/String.juvix b/Stdlib/Data/String.juvix
index 8744f92f..bbd8b80b 100644
--- a/Stdlib/Data/String.juvix
+++ b/Stdlib/Data/String.juvix
@@ -16,8 +16,7 @@ module StringTraits;
 
   Show : Show.Show String :=
     let
-      go : String -> String;
-      go s := "\"" ++str s ++str "\"";
+      go (s : String) : String := "\"" ++str s ++str "\"";
     in Show.mkShow go;
 
 end;
diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix
index b8acd7a2..e6dcb294 100644
--- a/Stdlib/Function.juvix
+++ b/Stdlib/Function.juvix
@@ -8,62 +8,35 @@ syntax operator ∘ composition;
 
 --- Function composition.
 {-# inline: 2 #-}
-∘
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (B → C)
-    → (A → B)
-    → A
-    → C
-  | f g x := f (g x);
+∘ {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);
 
 --- Always returns the first argument.
 {-# inline: 1 #-}
-const : {A : Type} → {B : Type} → A → B → A
-  | a _ := a;
+const {A B} (a : A) (_ : B) : A := a;
 
 --- The identity function.
-id : {A : Type} → A → A
-  | a := a;
+id {A} (a : A) : A := a;
 
 --- Swaps the order of the arguments of the given function.
 {-# inline: 1 #-}
-flip
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (A → B → C)
-    → B
-    → A
-    → C
-  | f b a := f a b;
+flip {A B C} (f : A → B → C) (b : B) (a : A) : C := f a b;
 
 syntax operator $ rapp;
 
 --- Application operator with right associativity. Usually used as a syntactical
 --- facility.
-$ : {A : Type} → {B : Type} → (A → B) → A → B
-  | f x := f x;
+$ {A B} (f : A → B) (x : A) : B := f x;
 
 --- Applies a function n times.
-iterate : {A : Type} -> Nat -> (A -> A) -> A -> A
+iterate {A} : Nat -> (A -> A) -> A -> A
   | zero _ a := a
   | (suc n) f a := iterate n f (f a);
 
 syntax operator on lapp;
 
 {-# inline: 2 #-}
-on
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (B → B → C)
-    → (A → B)
-    → A
-    → A
-    → C
-  | f g a b := 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/Bool.juvix b/Stdlib/System/IO/Bool.juvix
index 27d281c7..0fd5a9bb 100644
--- a/Stdlib/System/IO/Bool.juvix
+++ b/Stdlib/System/IO/Bool.juvix
@@ -7,5 +7,5 @@ import Stdlib.System.IO.String open;
 builtin bool-print
 axiom printBool : Bool → IO;
 
-printBoolLn : Bool → IO
-  | b := 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 e5125648..ed5ea299 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 : Int → IO
-  | i := 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 ccb0137b..8322fd4f 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 : Nat → IO
-  | n := 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 3bfade37..a949f18c 100644
--- a/Stdlib/System/IO/String.juvix
+++ b/Stdlib/System/IO/String.juvix
@@ -9,5 +9,5 @@ axiom printString : String → IO;
 builtin IO-readline
 axiom readLn : (String → IO) → IO;
 
-printStringLn : String → IO
-  | s := printString s >> printString "\n";
+printStringLn (s : String) : IO :=
+  printString s >> printString "\n";
diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
index 1ccb26cb..7f6c7124 100644
--- a/Stdlib/Trait/Eq.juvix
+++ b/Stdlib/Trait/Eq.juvix
@@ -6,5 +6,5 @@ import Stdlib.Data.Bool.Base open;
 type Eq (A : Type) :=
   | mkEq : (A -> A -> Bool) -> Eq A;
 
-eq : {A : Type} -> Eq A -> A -> A -> Bool
+eq {A} : Eq A -> A -> A -> Bool
   | (mkEq f) := f;
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index 58a8bf8a..f009deb9 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -23,5 +23,5 @@ isGT : Ordering → Bool
 type Ord (A : Type) :=
   | mkOrd : (A -> A -> Ordering) -> Ord A;
 
-cmp : {A : Type} -> Ord A -> A -> A -> Ordering
+cmp {A} : Ord A -> A -> A -> Ordering
   | (mkOrd f) := f;
diff --git a/Stdlib/Trait/Show.juvix b/Stdlib/Trait/Show.juvix
index 973fd1c5..de53aeaf 100644
--- a/Stdlib/Trait/Show.juvix
+++ b/Stdlib/Trait/Show.juvix
@@ -5,5 +5,5 @@ import Stdlib.Data.String.Base open;
 type Show (A : Type) :=
   | mkShow : (A -> String) -> Show A;
 
-show : {A : Type} -> Show A -> A -> String
+show {A} : Show A -> A -> String
   | (mkShow f) := f;
diff --git a/test/Makefile b/test/Makefile
index dfc17f59..ccc72c5a 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -3,7 +3,7 @@ all: test
 
 deps/quickcheck:
 	@mkdir -p deps/
-	@git clone --branch v0.6.3 --depth 1 https://github.com/anoma/juvix-quickcheck.git deps/quickcheck
+	@git clone --branch update-for-0.5.0 --depth 1 https://github.com/anoma/juvix-quickcheck.git deps/quickcheck
 	$(MAKE) -C deps/quickcheck deps
 
 build/Test: $(shell find ../ -name "*.juvix") $(wildcard deps/**/*.juvix) Test.juvix deps/quickcheck
diff --git a/test/Test.juvix b/test/Test.juvix
index 8cb45970..0be097b6 100644
--- a/test/Test.juvix
+++ b/test/Test.juvix
@@ -15,142 +15,136 @@ import Data.Int open;
 import Test.QuickCheckTest as QC;
 import Test.Arb as QC;
 
-prop-reverseDoesNotChangeLength : List Int -> Bool;
-prop-reverseDoesNotChangeLength xs :=
-  length (reverse xs) Nat.== length xs;
-
-prop-reverseReverseIsIdentity : List Int -> Bool;
-prop-reverseReverseIsIdentity xs :=
-  eqListInt xs (reverse (reverse xs));
-
-prop-tailLengthOneLess : List Int -> Bool;
-prop-tailLengthOneLess xs :=
-  null xs
-    || ofNat (length (tail xs)) == intSubNat (length xs) 1;
-
-prop-splitAtRecombine : Nat -> List Int -> Bool;
-prop-splitAtRecombine n xs :=
-  case splitAt n xs
-    | lhs, rhs := eqListInt xs (lhs ++ rhs);
-
-prop-splitAtLength : Nat -> List Int -> Bool;
-prop-splitAtLength n xs :=
-  case splitAt
-    n
-    (xs ++ replicate (sub n (length xs)) (ofNat 0))
-    | lhs, rhs :=
-      length lhs Nat.== n
-        && length rhs Nat.== sub (length xs) n;
+prop-reverseDoesNotChangeLength : List Int -> Bool
+  | xs := length (reverse xs) Nat.== length xs;
+
+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;
+
+prop-splitAtRecombine : Nat -> List Int -> Bool
+  | n xs :=
+    case splitAt n xs
+      | 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))
+      | lhs, rhs :=
+        length lhs Nat.== n
+          && length rhs Nat.== sub (length xs) n;
 -- Make sure the list has length at least n
 
-prop-mergeSumLengths : List Int -> List Int -> Bool;
-prop-mergeSumLengths xs ys :=
-  length xs Nat.+ length ys
-    Nat.== length (merge (IntTraits.Ord) xs ys);
-
-prop-partition : List Int -> (Int -> Bool) -> Bool;
-prop-partition xs p :=
-  case partition p xs
-    | lhs, rhs :=
-      all p lhs
-        && not (any p rhs)
-        && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
-
-prop-distributive : Int -> Int -> (Int -> Int) -> Bool;
-prop-distributive a b f := f (a + b) == f a + f b;
-
-prop-add-sub : Int -> Int -> Bool;
-prop-add-sub a b := a == a + b - b;
-
-prop-add-sub-bad : Int -> Int -> Bool;
-prop-add-sub-bad a b := a == 2;
-
-prop-gcd-bad : Int -> Int -> Bool;
-prop-gcd-bad a b := gcd a b > 1;
-
-prop-equal-compare-to-eq : Nat -> Bool;
-prop-equal-compare-to-eq a := Ord.isEQ (Nat.compare a a);
-
-prop-sort : (List Int -> List Int) -> List Int -> Bool;
-prop-sort sort xs :=
-  let
-    sorted : List Int := sort xs;
-    isSorted : List Int -> Bool;
-    isSorted nil := true;
-    isSorted (_ :: nil) := true;
-    isSorted (x :: y :: xs) := x <= y && isSorted (y :: xs);
-  in length sorted Nat.== length xs
-    && eqListInt sorted (sort sorted)
-    && isSorted sorted;
-
-prop-zip : List Int -> List Int -> Bool;
-prop-zip xs ys :=
-  let
-    zs : List (Int × Int) := zip xs ys;
-    expectedLen : Nat := Nat.min (length xs) (length ys);
-  in length zs Nat.== expectedLen
-    && 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 f xs ys :=
-  let
-    zs : List Int := zipWith f xs ys;
-    zsFlip : List Int := zipWith (flip f) ys xs;
-    expectedLen : Nat := Nat.min (length xs) (length ys);
-  in length zs Nat.== expectedLen
-    && eqListInt zs zsFlip
-    && eqListInt (map λ {x := f x x} xs) (zipWith f xs xs);
-
-prop-snoc : List Int -> Int -> Bool;
-prop-snoc xs x :=
-  let
-    snoc-x : List Int := snoc xs x;
-  in eqListInt snoc-x (reverse (x :: reverse xs));
-
-prop-drop : Nat -> List Int -> Bool;
-prop-drop n xs :=
-  let
-    drop-n : List Int;
-    drop-n := drop n xs;
-  in length drop-n Nat.<= length xs
-    && eqListInt (drop n (drop n xs)) (drop (2 Nat.* n) xs);
+prop-mergeSumLengths : List Int -> List Int -> Bool
+  | xs ys :=
+    length xs Nat.+ length ys
+      Nat.== length (merge (IntTraits.Ord) xs ys);
+
+prop-partition : List Int -> (Int -> Bool) -> Bool
+  | xs p :=
+    case partition p xs
+      | 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;
+
+prop-add-sub : Int -> Int -> Bool
+  | a b := a == a + b - b;
+
+prop-add-sub-bad : Int -> Int -> Bool
+  | a b := a == 2;
+
+prop-gcd-bad : Int -> Int -> Bool
+  | a b := gcd a b > 1;
+
+prop-equal-compare-to-eq : Nat -> Bool
+  | a := Ord.isEQ (Nat.compare a a);
+
+prop-sort : (List Int -> List Int) -> List Int -> Bool
+  | sort xs :=
+    let
+      sorted : List Int := sort xs;
+      isSorted : List Int -> Bool
+        | nil := true
+        | (_ :: nil) := true
+        | (x :: y :: xs) := x <= y && isSorted (y :: xs);
+    in length sorted Nat.== length xs
+      && eqListInt sorted (sort sorted)
+      && isSorted sorted;
+
+prop-zip : List Int -> List Int -> Bool
+  | xs ys :=
+    let
+      zs : List (Int × Int) := zip xs ys;
+      expectedLen : Nat := Nat.min (length xs) (length ys);
+    in length zs Nat.== expectedLen
+      && eqListInt (take expectedLen xs) (map fst zs)
+      && eqListInt (take expectedLen ys) (map snd zs);
+
+prop-zipWith
+  : (Int -> Int -> Int) -> List Int -> List Int -> Bool
+  | f xs ys :=
+    let
+      zs : List Int := zipWith f xs ys;
+      zsFlip : List Int := zipWith (flip f) ys xs;
+      expectedLen : Nat := Nat.min (length xs) (length ys);
+    in length zs Nat.== expectedLen
+      && eqListInt zs zsFlip
+      && eqListInt (map λ {x := f x x} xs) (zipWith f xs xs);
+
+prop-snoc : List Int -> Int -> Bool
+  | xs x :=
+    let
+      snoc-x : List Int := snoc xs x;
+    in eqListInt snoc-x (reverse (x :: reverse xs));
+
+prop-drop : Nat -> List Int -> Bool
+  | n xs :=
+    let
+      drop-n : List Int := drop n xs;
+    in length drop-n Nat.<= length xs
+      && eqListInt (drop n (drop n xs)) (drop (2 Nat.* n) xs);
 
 -- Assumption: The input list represents a rectangular matrix
-prop-transposeMatrixId : List (List Int) -> Bool;
-prop-transposeMatrixId xs :=
-  eq
-    (ListTraits.Eq (ListTraits.Eq (IntTraits.Eq)))
-    xs
-    (transpose (transpose xs));
+prop-transposeMatrixId : List (List Int) -> Bool
+  | xs :=
+    eq
+      (ListTraits.Eq (ListTraits.Eq (IntTraits.Eq)))
+      xs
+      (transpose (transpose xs));
 
 -- Assumption: The input list represents a rectangular matrix
-prop-transposeMatrixDimensions : List (List Int) -> Bool;
-prop-transposeMatrixDimensions xs :=
-  let
-    txs : List (List Int) := transpose xs;
-    checkTxsRowXsCol :
-      Bool :=
+prop-transposeMatrixDimensions : List (List Int) -> Bool
+  | xs :=
+    let
+      txs : List (List Int) := transpose xs;
+      checkTxsRowXsCol : Bool :=
         case xs
           | x :: _ := length txs Nat.== length x
           | _ := null txs;
-    checkXsRowTxsCol :
-      Bool :=
+      checkXsRowTxsCol : Bool :=
         case txs
           | tx :: _ := length xs Nat.== length tx
           | _ := null xs;
-  in checkTxsRowXsCol && checkXsRowTxsCol;
+    in checkTxsRowXsCol && checkXsRowTxsCol;
 
-sortTest : String -> (List Int -> List Int) -> QC.Test;
-sortTest sortName sort :=
-  QC.mkTest
-    (QC.testableFunction QC.argumentListInt QC.testableBool)
-    ("sort properties: " ++str sortName)
-    (prop-sort sort);
+sortTest : String -> (List Int -> List Int) -> QC.Test
+  | sortName sort :=
+    QC.mkTest
+      (QC.testableFunction QC.argumentListInt QC.testableBool)
+      ("sort properties: " ++str sortName)
+      (prop-sort sort);
 
-dropTest : QC.Test;
-dropTest :=
+dropTest : QC.Test :=
   QC.mkTest
     (QC.testableFunction
       QC.argumentNat
@@ -158,8 +152,7 @@ dropTest :=
     "drop properties"
     prop-drop;
 
-snocTest : QC.Test;
-snocTest :=
+snocTest : QC.Test :=
   QC.mkTest
     (QC.testableFunction
       QC.argumentListInt
@@ -167,106 +160,91 @@ snocTest :=
     "snoc properties"
     prop-snoc;
 
-zipTest : QC.Test;
-zipTest :=
+zipTest : QC.Test :=
   QC.mkTest
     QC.testableListIntListInt
     "zip properties"
     prop-zip;
 
-zipWithTest : QC.Test;
-zipWithTest :=
+zipWithTest : QC.Test :=
   QC.mkTest
     QC.testableHofIntIntListIntListInt
     "zipWith properties"
     prop-zipWith;
 
-equalCompareToEqTest : QC.Test;
-equalCompareToEqTest :=
+equalCompareToEqTest : QC.Test :=
   QC.mkTest
     (QC.testableFunction QC.argumentNat QC.testableBool)
     "equal Nats compare to EQ"
     prop-equal-compare-to-eq;
 
-gcdNoCoprimeTest : QC.Test;
-gcdNoCoprimeTest :=
+gcdNoCoprimeTest : QC.Test :=
   QC.mkTest
     QC.testableBinaryInt
     "no integers are coprime"
     prop-gcd-bad;
 
-partitionTest : QC.Test;
-partitionTest :=
+partitionTest : QC.Test :=
   QC.mkTest
     QC.testableListIntHofIntBool
     "partition: recombination of the output equals the input"
     prop-partition;
 
-testDistributive : QC.Test;
-testDistributive :=
+testDistributive : QC.Test :=
   QC.mkTest
     QC.testableIntIntHofIntInt
     "all functions are distributive over +"
     prop-distributive;
 
-reverseLengthTest : QC.Test;
-reverseLengthTest :=
+reverseLengthTest : QC.Test :=
   QC.mkTest
     QC.testableListInt
     "reverse preserves length"
     prop-reverseDoesNotChangeLength;
 
-reverseReverseIdTest : QC.Test;
-reverseReverseIdTest :=
+reverseReverseIdTest : QC.Test :=
   QC.mkTest
     QC.testableListInt
     "reverse of reverse is identity"
     prop-reverseReverseIsIdentity;
 
-splitAtRecombineTest : QC.Test;
-splitAtRecombineTest :=
+splitAtRecombineTest : QC.Test :=
   QC.mkTest
     QC.testableNatListInt
     "splitAt: recombination of the output is equal to the input list"
     prop-splitAtRecombine;
 
-splitAtLengthTest : QC.Test;
-splitAtLengthTest :=
+splitAtLengthTest : QC.Test :=
   QC.mkTest
     QC.testableNatListInt
     "splitAt: Check lengths of output if the input Nat is greater than the length of the input list"
     prop-splitAtLength;
 
-mergeSumLengthsTest : QC.Test;
-mergeSumLengthsTest :=
+mergeSumLengthsTest : QC.Test :=
   QC.mkTest
     QC.testableListIntListInt
     "merge: sum of the lengths of input lists is equal to the length of output list"
     prop-mergeSumLengths;
 
-tailLengthOneLessTest : QC.Test;
-tailLengthOneLessTest :=
+tailLengthOneLessTest : QC.Test :=
   QC.mkTest
     QC.testableListInt
     "tail: length of output is one less than input unless empty"
     prop-tailLengthOneLess;
 
-transposeMatrixIdTest : QC.Test;
-transposeMatrixIdTest :=
+transposeMatrixIdTest : QC.Test :=
   QC.mkTest
     (QC.testableFunction QC.argumentMatrixInt QC.testableBool)
     "transpose: recrangular matrix has property transpose . transpose = id"
     prop-transposeMatrixId;
 
-transposeMatrixDimentionsTest : QC.Test;
-transposeMatrixDimentionsTest :=
+transposeMatrixDimentionsTest : QC.Test :=
   QC.mkTest
     (QC.testableFunction QC.argumentMatrixInt QC.testableBool)
     "transpose: transpose swaps dimensions"
     prop-transposeMatrixDimensions;
 
-main : IO;
-main :=
+main : IO :=
   readLn
     \ {seed :=
       QC.runTestsIO
diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix
index cf334f86..5833b2c1 100644
--- a/test/Test/Arb.juvix
+++ b/test/Test/Arb.juvix
@@ -6,41 +6,39 @@ import Test.QuickCheck.Arbitrary open;
 import Test.QuickCheck.Gen open;
 import Data.Random open;
 
-arbitrarySizedList :
-  {A : Type} -> Nat -> Arbitrary A -> Arbitrary (List A);
-arbitrarySizedList {A} size (arbitrary g) :=
-  arbitrary
-    (gen
-      \ {rand :=
-        let
-          randList : StdGen -> Nat -> List A;
-          randList _ zero := nil;
-          randList r (suc n) :=
-            let
-              rSplit : StdGen × StdGen;
-              rSplit := stdSplit r;
-              r1 : StdGen := fst rSplit;
-              r2 : StdGen := snd rSplit;
-            in runGen g r1 :: randList r2 n;
-        in randList rand size});
+arbitrarySizedList
+  : {A : Type} -> Nat -> Arbitrary A -> Arbitrary (List A)
+  | {A} size (arbitrary g) :=
+    arbitrary
+      (gen
+        \ {rand :=
+          let
+            randList : StdGen -> Nat -> List A
+              | _ zero := nil
+              | r (suc n) :=
+                let
+                  rSplit : StdGen × StdGen := stdSplit r;
+                  r1 : StdGen := fst rSplit;
+                  r2 : StdGen := snd rSplit;
+                in runGen g r1 :: randList r2 n;
+          in randList rand size});
 
 --- Generate an arbitrary rectangular matrix
-arbitraryMatrix :
-  {A : Type} -> Arbitrary A -> Arbitrary (List (List A));
-arbitraryMatrix {A} arbA :=
-  arbitrary
-    (gen
-      \ {rand :=
-        let
-          randSplit : StdGen × StdGen := stdSplit rand;
-          rand1 : StdGen := fst randSplit;
-          rand2 : StdGen := snd randSplit;
-          cols : Nat := fst (randNat rand1 1 10);
-          arbRow : Arbitrary (List A) := arbitrarySizedList cols arbA;
-        in runArb (arbitraryList arbRow) rand2});
+arbitraryMatrix
+  : {A : Type} -> Arbitrary A -> Arbitrary (List (List A))
+  | {A} arbA :=
+    arbitrary
+      (gen
+        \ {rand :=
+          let
+            randSplit : StdGen × StdGen := stdSplit rand;
+            rand1 : StdGen := fst randSplit;
+            rand2 : StdGen := snd randSplit;
+            cols : Nat := fst (randNat rand1 1 10);
+            arbRow : Arbitrary (List A) := arbitrarySizedList cols arbA;
+          in runArb (arbitraryList arbRow) rand2});
 
-argumentMatrixInt : Argument (List (List Int));
-argumentMatrixInt :=
+argumentMatrixInt : Argument (List (List Int)) :=
   argument
     (ListTraits.Show (ListTraits.Show IntTraits.Show))
     (arbitraryMatrix arbitraryInt);