diff --git a/Stdlib/Cairo/Ec.juvix b/Stdlib/Cairo/Ec.juvix
index fcf44b71..a3de922d 100644
--- a/Stdlib/Cairo/Ec.juvix
+++ b/Stdlib/Cairo/Ec.juvix
@@ -8,6 +8,7 @@ module Stdlib.Cairo.Ec;
 
 import Stdlib.Data.Field open;
 import Stdlib.Data.Bool open;
+import Stdlib.Data.Pair open;
 
 module StarkCurve;
   ALPHA : Field := 1;
@@ -37,77 +38,80 @@ module Internal;
 end;
 
 --- Checks if an EC point is on the STARK curve.
-isOnCurve : Point -> Bool
-  | (mkPoint x y) :=
-    if
-      | y == 0 := x == 0
-      | 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
-  | p@(mkPoint x y) :=
-    if
-      | y == 0 := p
-      | else :=
-        let
-          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
-        };
+isOnCurve (point : Point) : Bool :=
+  case point of
+    mkPoint x y :=
+      if
+        | y == 0 := x == 0
+        | else := y * y == (x * x + StarkCurve.ALPHA) * x + StarkCurve.BETA;
+
+--- Doubles a valid `point` (computes point + point) on the elliptic curve.
+double (point : Point) : Point :=
+  case point of
+    mkPoint x y :=
+      if
+        | y == 0 := point
+        | else :=
+          let
+            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
+          };
 
 --- Adds two valid points on the EC.
-add : Point -> Point -> Point
-  | p@(mkPoint x1 y1) q@(mkPoint x2 y2) :=
-    if
-      | y1 == 0 := q
-      | y2 == 0 := p
-      | x1 == x2 :=
-        if
-          | y1 == y2 := double p
-          | else := mkPoint 0 0
-      | else :=
-        let
-          slope := (y1 - y2) / (x1 - x2);
-          r_x := slope * slope - x1 - x2;
-          r_y := slope * (x1 - r_x) - y1;
-        in mkPoint r_x r_y;
-
---- Subtracts a point from another on the EC.
-sub (p q : Point) : Point := add p q@Point{y := 0 - y};
-
---- Computes p + m * q on the elliptic curve.
+add (point1 point2 : Point) : Point :=
+  case point1, point2 of
+    mkPoint x1 y1, mkPoint x2 y2 :=
+      if
+        | y1 == 0 := point2
+        | y2 == 0 := point1
+        | x1 == x2 :=
+          if
+            | y1 == y2 := double point1
+            | else := mkPoint 0 0
+        | else :=
+          let
+            slope := (y1 - y2) / (x1 - x2);
+            r_x := slope * slope - x1 - x2;
+            r_y := slope * (x1 - r_x) - y1;
+          in mkPoint r_x r_y;
+
+--- Subtracts point2 from point1 on the EC.
+sub (point1 point2 : Point) : Point := add point1 point2@Point{y := 0 - y};
+
+--- Computes point1 + alpha * point2 on the elliptic curve.
 --- Because the EC operation builtin cannot handle inputs where additions of points with the same x
 --- coordinate arise during the computation, this function adds and subtracts a nondeterministic
 --- point s to the computation, so that regardless of input, the probability that such additions
 --- arise will become negligibly small.
 --- The precise computation is therefore:
---- ((p + s) + m * q) - s
---- so that the inputs to the builtin itself are (p + s), m, and q.
+--- ((point1 + s) + alpha * point2) - s
+--- so that the inputs to the builtin itself are (point1 + s), alpha, and point2.
 ---
 --- Arguments:
---- p - an EC point.
---- m - the multiplication coefficient of q (a field element).
---- q - an EC point.
+--- point1 - an EC point.
+--- alpha - the multiplication coefficient of point2 (a field element).
+--- point2 - an EC point.
 ---
 --- Returns:
---- p + m * q.
+--- point1 + alpha * point2.
 ---
 --- Assumptions:
---- p and q are valid points on the curve.
-addMul (p : Point) (m : Field) (q : Point) : Point :=
+--- point1 and point2 are valid points on the curve.
+addMul (point1 : Point) (alpha : Field) (point2 : Point) : Point :=
   if
-    | Point.y q == 0 := p
+    | Point.y point2 == 0 := point1
     | else :=
       let
         s : Point := Internal.randomEcPoint;
-        r : Point := Internal.ecOp (add p s) m q;
+        r : Point := Internal.ecOp (add point1 s) alpha point2;
       in sub r s;
 
---- Computes m * p on the elliptic curve.
-mul (m : Field) (p : Point) : Point := addMul (mkPoint 0 0) m p;
+--- Computes alpha * point on the elliptic curve.
+mul (alpha : Field) (point : Point) : Point := addMul (mkPoint 0 0) alpha point;
 
 module Operators;
   import Stdlib.Data.Fixity open;
diff --git a/Stdlib/Cairo/Poseidon.juvix b/Stdlib/Cairo/Poseidon.juvix
index a025b2eb..ebaded3d 100644
--- a/Stdlib/Cairo/Poseidon.juvix
+++ b/Stdlib/Cairo/Poseidon.juvix
@@ -27,11 +27,11 @@ poseidonHash2 (x y : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseido
 
 --- Hashes n elements and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHashList (lst : List Field) : Field :=
+poseidonHashList (list : 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 }
       | (x1 :: x2 :: xs) :=
         go (poseidonHash acc@PoseidonState{   s0 := s0 + x1; s1 := s1 + x2 }) xs;
-  in PoseidonState.s0 (go (mkPoseidonState 0 0 0) lst);
+  in PoseidonState.s0 (go (mkPoseidonState 0 0 0) list);
diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix
index e5876a06..6a70de9b 100644
--- a/Stdlib/Data/BinaryTree.juvix
+++ b/Stdlib/Data/BinaryTree.juvix
@@ -4,17 +4,21 @@ import Stdlib.Data.Nat open;
 import Stdlib.Data.List open;
 
 type BinaryTree (A : Type) :=
-  | leaf : BinaryTree A
-  | node : BinaryTree A -> A -> BinaryTree A -> BinaryTree A;
+  | leaf
+  | node {
+      left : BinaryTree A;
+      element : A;
+      right : BinaryTree A
+    };
 
---- fold a tree in depth first order
-fold {A B} (f : A -> B -> B -> B) (acc : B) : BinaryTree A -> B :=
+--- fold a tree in depth-first order
+fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B :=
   let
     go (acc : B) : BinaryTree A -> B
       | leaf := acc
       | (node l a r) := f a (go acc l) (go acc r);
-  in go acc;
+  in go acc tree;
 
-length : {A : Type} -> BinaryTree A -> Nat := fold λ {_ l r := 1 + l + r} 0;
+length {A} (tree : BinaryTree A) : Nat := fold \ {_ l r := 1 + l + r} 0 tree;
 
-to-list : {A : Type} -> BinaryTree A -> List A := fold λ {e ls rs := e :: ls ++ rs} nil;
+toList {A} (tree : BinaryTree A) : List A := fold \ {e ls rs := e :: ls ++ rs} nil tree;
diff --git a/Stdlib/Data/Bool.juvix b/Stdlib/Data/Bool.juvix
index bfc5d891..6aa14b87 100644
--- a/Stdlib/Data/Bool.juvix
+++ b/Stdlib/Data/Bool.juvix
@@ -1,6 +1,8 @@
 module Stdlib.Data.Bool;
 
 import Stdlib.Data.Bool.Base open public;
+import Stdlib.Data.Pair.Base open;
+import Stdlib.Data.String.Base open;
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
@@ -8,28 +10,31 @@ import Stdlib.Trait.Show open;
 {-# specialize: true, inline: case #-}
 instance
 boolEqI : Eq Bool :=
-  mkEq
-    λ {
-      | true true := true
-      | false false := true
-      | _ _ := false
-    };
+  mkEq@{
+    eq (x y : Bool) : Bool :=
+      case x, y of
+        | true, true := true
+        | false, false := true
+        | _ := false
+  };
 
 {-# specialize: true, inline: case #-}
 instance
 boolOrdI : Ord Bool :=
-  mkOrd
-    λ {
-      | false false := EQ
-      | false true := LT
-      | true false := GT
-      | true true := EQ
-    };
+  mkOrd@{
+    cmp (x y : Bool) : Ordering :=
+      case x, y of
+        | false, false := Equal
+        | false, true := LessThan
+        | true, false := GreaterThan
+        | true, true := Equal
+  };
 
 instance
 showBoolI : Show Bool :=
-  mkShow
-    λ {
-      | true := "true"
-      | false := "false"
-    };
+  mkShow@{
+    show (x : Bool) : String :=
+      if
+        | x := "true"
+        | else := "false"
+  };
diff --git a/Stdlib/Data/Bool/Base.juvix b/Stdlib/Data/Bool/Base.juvix
index d266726d..75fe8a63 100644
--- a/Stdlib/Data/Bool/Base.juvix
+++ b/Stdlib/Data/Bool/Base.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Fixity open;
 
 --- Logical negation.
 {-# isabelle-function: {name: "\\<not>"} #-}
-not : Bool → Bool
+not : Bool -> Bool
   | true := false
   | false := true;
 
@@ -13,7 +13,7 @@ syntax operator || logical;
 
 --- Logical disjunction. Evaluated lazily. Cannot be partially applied
 builtin bool-or
-|| : Bool → Bool → Bool
+|| : Bool -> Bool -> Bool
   | true _ := true
   | false a := a;
 
@@ -21,13 +21,13 @@ syntax operator && logical;
 
 --- Logical conjunction. Evaluated lazily. Cannot be partially applied.
 builtin bool-and
-&& : Bool → Bool → Bool
+&& : Bool -> Bool -> Bool
   | true a := a
   | false _ := false;
 
 --- Returns the first argument if ;true;, otherwise it returns the second argument. Evaluated lazily. Cannot be partially applied.
 builtin bool-if
-ite : {A : Type} → Bool → A → A → A
+ite : {A : Type} -> Bool -> A -> A -> A
   | true a _ := a
   | false _ b := b;
 
diff --git a/Stdlib/Data/Byte.juvix b/Stdlib/Data/Byte.juvix
index 89cfab6c..99bb444c 100644
--- a/Stdlib/Data/Byte.juvix
+++ b/Stdlib/Data/Byte.juvix
@@ -17,7 +17,7 @@ eqByteI : Eq Byte := mkEq (Byte.==);
 instance
 showByteI : Show Byte :=
   mkShow@{
-    show := Byte.toNat >> Show.show
+    show (x : Byte) : String := Show.show (Byte.toNat x)
   };
 
 {-# specialize: true, inline: case #-}
diff --git a/Stdlib/Data/Int/Base.juvix b/Stdlib/Data/Int/Base.juvix
index f3cb68d2..bfc4fcd5 100644
--- a/Stdlib/Data/Int/Base.juvix
+++ b/Stdlib/Data/Int/Base.juvix
@@ -16,9 +16,10 @@ type Int :=
     negSuc Nat;
 
 --- Converts an ;Int; to a ;Nat;. If the ;Int; is negative, it returns ;zero;.
-toNat : Int -> Nat
-  | (ofNat n) := n
-  | (negSuc _) := zero;
+toNat (int : Int) : Nat :=
+  case int of
+    | ofNat n := n
+    | negSuc _ := zero;
 
 --- Non-negative predicate for ;Int;s.
 builtin int-nonneg
@@ -88,6 +89,7 @@ mod : Int -> Int -> Int
   | (negSuc m) (negSuc n) := negNat (Nat.mod (suc m) (suc n));
 
 --- Absolute value
-abs : Int -> Nat
-  | (ofNat n) := n
-  | (negSuc n) := suc n;
+abs (int : Int) : Nat :=
+  case int of
+    | ofNat n := n
+    | negSuc n := suc n;
diff --git a/Stdlib/Data/Int/Ord.juvix b/Stdlib/Data/Int/Ord.juvix
index 31fdf058..cf51476b 100644
--- a/Stdlib/Data/Int/Ord.juvix
+++ b/Stdlib/Data/Int/Ord.juvix
@@ -4,7 +4,7 @@ import Stdlib.Data.Fixity open;
 
 import Stdlib.Data.Int.Base open;
 import Stdlib.Data.Bool.Base open;
-import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering};
+import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering};
 
 import Stdlib.Data.Nat.Base as Nat;
 import Stdlib.Data.Nat.Ord as Nat;
@@ -49,9 +49,9 @@ syntax operator >= comparison;
 {-# inline: true #-}
 compare (m n : Int) : Ordering :=
   if
-    | m == n := EQ
-    | m < n := LT
-    | else := GT;
+    | m == n := Equal
+    | m < n := LessThan
+    | else := GreaterThan;
 
 --- Returns the smallest ;Int;.
 min (x y : Int) : Int := ite (x < y) x y;
diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
index e31a7b06..6596def2 100644
--- a/Stdlib/Data/List.juvix
+++ b/Stdlib/Data/List.juvix
@@ -27,18 +27,20 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
       | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false;
   in mkEq go;
 
+isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool := isElement (Eq.eq) elem list;
+
 instance
 ordListI {A} {{Ord A}} : Ord (List A) :=
   let
     go : List A -> List A -> Ordering
-      | nil nil := EQ
-      | nil _ := LT
-      | _ nil := GT
+      | nil nil := Equal
+      | nil _ := LessThan
+      | _ nil := GreaterThan
       | (x :: xs) (y :: ys) :=
         case Ord.cmp x y of
-          | LT := LT
-          | GT := GT
-          | EQ := go xs ys;
+          | LessThan := LessThan
+          | GreaterThan := GreaterThan
+          | Equal := go xs ys;
   in mkOrd go;
 
 instance
@@ -47,11 +49,12 @@ showListI {A} {{Show A}} : Show (List A) :=
     go : List A -> String
       | nil := "nil"
       | (x :: xs) := Show.show x ++str " :: " ++str go xs;
-  in mkShow
-    λ {
-      | nil := "nil"
-      | s := "(" ++str go s ++str ")"
-    };
+  in mkShow@{
+    show (list : List A) : String :=
+      case list of
+        | nil := "nil"
+        | s := "(" ++str go s ++str ")"
+  };
 
 {-# specialize: true, inline: case #-}
 instance
@@ -80,7 +83,7 @@ instance
 applicativeListI : Applicative List :=
   mkApplicative@{
     pure {A} (a : A) : List A := [a];
-    ap {A B} : List (A -> B) -> List A -> List B
+    ap {A B} : (listOfFuns : List (A -> B)) -> (listOfAs : List A) -> List B
       | [] _ := []
       | (f :: fs) l := map f l ++ ap fs l
   };
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index d472078f..e900074f 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/Stdlib/Data/List/Base.juvix
@@ -9,63 +9,63 @@ import Stdlib.Data.Maybe.Base open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Data.Pair.Base open;
 
---- 𝒪(𝓃). Returns ;true; if the given
---- object is in the ;List;.
+--- 𝒪(𝓃). Returns ;true; if the given object elem is in the ;List;.
 {-# specialize: [1] #-}
-elem {A} (eq : A → A → Bool) (s : A) : List A → Bool
+isElement {A} (eq : A -> A -> Bool) (elem : A) : (list : List A) -> Bool
   | nil := false
-  | (x :: xs) := eq s x || elem eq s xs;
+  | (x :: xs) := eq elem x || isElement eq elem xs;
 
 --- 𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or
---- nothing if there's no such element.
+--- nothing if there is no such element.
 {-# specialize: [1] #-}
-find {A} (predicate : A → Bool) : List A → Maybe A
+find {A} (predicate : A -> Bool) : (list : List A) -> Maybe A
   | nil := nothing
   | (x :: xs) :=
     if
       | predicate x := just x
       | else := find predicate xs;
 
---- Right-associative fold.
-{-# specialize: [1] #-}
-liftFoldr {A B} (f : A → B → B) (z : B) : List A → B
-  | nil := z
-  | (h :: hs) := f h (liftFoldr f z hs);
-
 syntax iterator listRfor {init := 1; range := 1};
 
 {-# specialize: [1] #-}
-listRfor {A B} (f : B → A → B) (acc : B) : List A → B
+listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> B
   | nil := acc
-  | (x :: xs) := f (listRfor f acc xs) x;
+  | (x :: xs) := fun (listRfor fun acc xs) x;
+
+--- Right-associative fold.
+{-# specialize: [1] #-}
+liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : B := listRfor (flip fun) acc list;
 
 --- Left-associative and tail-recursive fold.
 {-# specialize: [1] #-}
-listFoldl {A B} (f : B → A → B) (z : B) : List A → B
-  | nil := z
-  | (h :: hs) := listFoldl f (f z h) hs;
+listFoldl {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> B
+  | nil := acc
+  | (h :: hs) := listFoldl fun (fun acc h) hs;
 
 syntax iterator listFor {init := 1; range := 1};
 
 {-# inline: 0, isabelle-function: {name: "foldl"} #-}
-listFor : {A B : Type} → (B → A → B) → B → List A → B := listFoldl;
+listFor : {A B : Type} -> (B -> A -> B) -> B -> List A -> B := listFoldl;
 
 syntax iterator listMap {init := 0; range := 1};
 
 --- 𝒪(𝓃). Maps a function over each element of a ;List;.
 {-# specialize: [1] #-}
-listMap {A B} (f : A → B) : List A → List B
+listMap {A B} (fun : A -> B) : (list : List A) -> List B
   | nil := nil
-  | (h :: hs) := f h :: listMap f hs;
+  | (h :: hs) := fun h :: listMap fun 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} (f : A → Bool) : List A → List A
+filter {A} (predicate : A -> Bool) : (list : List A) -> List A
   | nil := nil
-  | (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs);
+  | (h :: hs) :=
+    if
+      | predicate h := h :: filter predicate hs
+      | else := filter predicate hs;
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
 length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc};
@@ -74,24 +74,25 @@ length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc};
 {-# isabelle-function: {name: "rev"} #-}
 reverse {A} (l : List A) : List A := listFor (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
+--- Returns a ;List; of length resultLength where every element is the given value.
+replicate {A} : (resultLength : Nat) -> (value : A) -> List A
   | zero _ := nil
   | (suc n) x := x :: replicate n x;
 
---- Takes the first n elements of a ;List;.
-take {A} : Nat → List A → List A
+--- Takes the first elemsNum elements of a ;List;.
+take {A} : (elemsNum : Nat) -> (list : List A) -> List A
   | (suc n) (x :: xs) := x :: take n xs
   | _ _ := nil;
 
---- Drops the first n elements of a ;List;.
-drop {A} : Nat → List A → List A
+--- Drops the first elemsNum elements of a ;List;.
+drop {A} : (elemsNum : Nat) -> (list : 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} : Nat → List A → Pair (List A) (List A)
+--- 𝒪(𝓃). Returns a tuple where first element is the
+--- prefix of the given list of length prefixLength and second element is the
+--- remainder of the ;List;.
+splitAt {A} : (prefixLength : Nat) -> (list : List A) -> Pair (List A) (List A)
   | _ nil := nil, nil
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
@@ -99,92 +100,108 @@ splitAt {A} : Nat → List A → Pair (List A) (List A)
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
 terminating
-merge {A} {{Ord A}} : List A → List A → List A
-  | xs@(x :: xs') ys@(y :: ys') :=
-    if
-      | isLT (Ord.cmp x y) := x :: merge xs' ys
-      | else := y :: merge xs ys'
-  | nil ys := ys
-  | xs nil := xs;
+merge {A} {{Ord A}} (list1 list2 : List A) : List A :=
+  case list1, list2 of
+    | xs@(x :: xs'), ys@(y :: ys') :=
+      if
+        | x < y := x :: merge xs' ys
+        | else := y :: merge xs ys'
+    | nil, ys := ys
+    | xs, nil := xs;
 
 --- 𝒪(𝓃). 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} (predicate : A → Bool) : (list : 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 predicate xs of
+      l1, l2 :=
+        if
+          | predicate x := x :: l1, l2
+          | else := l1, x :: l2;
 
 syntax operator ++ cons;
 
 --- Concatenates two ;List;s.
-++ : {A : Type} → List A → List A → List A
+++ : {A : Type} -> (list1 : List A) -> (list2 : List A) -> List A
   | nil ys := ys
   | (x :: xs) ys := x :: xs ++ ys;
 
 --- 𝒪(𝓃). Append an element.
-snoc {A} (xs : List A) (x : A) : List A := xs ++ x :: nil;
+snoc {A} (list : List A) (elem : A) : List A := list ++ elem :: nil;
 
 --- Concatenates a ;List; of ;List;s.
 {-# isabelle-function: {name: "concat"} #-}
-flatten : {A : Type} → List (List A) → List A := listFoldl (++) nil;
+flatten {A} (listOfLists : List (List A)) : List A := listFoldl (++) nil listOfLists;
 
---- 𝒪(𝓃). Inserts the given element before every element in the given ;List;.
-prependToAll {A} (sep : A) : List A → List A
+--- 𝒪(𝓃). Inserts the given separator before every element in the given ;List;.
+prependToAll {A} (separator : A) : (list : List A) -> List A
   | nil := nil
-  | (x :: xs) := sep :: x :: prependToAll sep xs;
+  | (x :: xs) := separator :: x :: prependToAll separator xs;
 
---- 𝒪(𝓃). Inserts the given element inbetween every two elements in the given ;List;.
-intersperse {A} (sep : A) : List A → List A
-  | nil := nil
-  | (x :: xs) := x :: prependToAll sep xs;
+--- 𝒪(𝓃). Inserts the given separator inbetween every two elements in the given ;List;.
+intersperse {A} (separator : A) (list : List A) : List A :=
+  case list of
+    | nil := nil
+    | x :: xs := x :: prependToAll separator xs;
 
 --- 𝒪(1). Drops the first element of a ;List;.
 {-# isabelle-function: {name: "tl"} #-}
-tail {A} : List A → List A
-  | (_ :: xs) := xs
-  | nil := nil;
+tail {A} (list : List A) : List A :=
+  case list of
+    | _ :: xs := xs
+    | nil := nil;
 
-head {A} (a : A) : List A -> A
-  | (x :: _) := x
-  | nil := a;
+head {A} (defaultValue : A) (list : List A) : A :=
+  case list of
+    | x :: _ := x
+    | nil := defaultValue;
 
 syntax iterator any {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.
 {-# specialize: [1] #-}
-any {A} (f : A → Bool) : List A → Bool
+any {A} (predicate : A -> Bool) : (list : List A) -> Bool
   | nil := false
-  | (x :: xs) := ite (f x) true (any f xs);
+  | (x :: xs) :=
+    if
+      | predicate x := true
+      | else := any predicate xs;
 
 syntax iterator all {init := 0; range := 1};
 
 --- 𝒪(𝓃). Returns ;true; if all elements of the ;List; satisfy the predicate.
 {-# specialize: [1] #-}
-all {A} (f : A -> Bool) : List A -> Bool
+all {A} (predicate : A -> Bool) : (list : List A) -> Bool
   | nil := true
-  | (x :: xs) := ite (f x) (all f xs) false;
+  | (x :: xs) :=
+    if
+      | predicate x := all predicate xs
+      | else := false;
 
 --- 𝒪(1). Returns ;true; if the ;List; is empty.
-null {A} : List A → Bool
-  | nil := true
-  | _ := false;
+null {A} (list : List A) : Bool :=
+  case list of
+    | 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} (f : A -> B -> C) : List A -> List B -> List C
+zipWith {A B C} (fun : A -> B -> C) : (listA : List A) -> (listB : List B) -> List C
   | nil _ := nil
   | _ nil := nil
-  | (x :: xs) (y :: ys) := f x y :: zipWith f xs ys;
+  | (x :: xs) (y :: ys) := fun x y :: zipWith fun xs ys;
 
 --- 𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists.
-zip {A B} : List A -> List B -> List (Pair A B)
+zip {A B} : (listA : List A) -> (listB : List B) -> List (Pair 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} {{Ord A}} (l : List A) : List A :=
+mergeSort {A} {{Ord A}} (list : List A) : List A :=
   let
     terminating
     go : Nat -> List A -> List A
@@ -197,22 +214,22 @@ mergeSort {A} {{Ord A}} (l : List A) : List A :=
           left : List A := fst splitXs;
           right : List A := snd splitXs;
         in merge (go len' left) (go (sub len len') right);
-  in go (length l) l;
+  in go (length list) list;
 
 --- On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in
 --- ascending order using the QuickSort algorithm.
 terminating
-quickSort {A} {{Ord A}} : List A → List A :=
+quickSort {A} {{Ord A}} (list : List A) : List A :=
   let
     terminating
-    go : 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;
-  in go;
+      | (x :: xs) := case partition \ {y := y < x} xs of l1, l2 := go l1 ++ x :: go l2;
+  in go list;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.
-catMaybes {A} : List (Maybe A) -> List A
+catMaybes {A} : (listOfMaybes : List (Maybe A)) -> List A
   | nil := nil
   | (just h :: hs) := h :: catMaybes hs
   | (nothing :: hs) := catMaybes hs;
@@ -221,10 +238,10 @@ 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 := listMap f >> flatten;
+concatMap {A B} (fun : A -> List B) (list : List A) : List B := flatten (listMap fun list);
 
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
-transpose {A} : List (List A) -> List (List A)
+transpose {A} : (listOfLists : List (List A)) -> List (List A)
   | nil := nil
   | (xs :: nil) := listMap λ {x := x :: nil} xs
   | (xs :: xss) := zipWith (::) xs (transpose xss);
diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix
index eb3995e3..841a030e 100644
--- a/Stdlib/Data/Map.juvix
+++ b/Stdlib/Data/Map.juvix
@@ -19,32 +19,44 @@ open AVL using {AVLTree};
 
 import Stdlib.Data.BinaryTree as Tree;
 
-type Binding A B := binding A B;
+type Binding Key Value :=
+  mkBinding {
+    key : Key;
+    value : Value
+  };
 
-key {A B} : Binding A B -> A
-  | (binding a _) := a;
+key {Key Value} (binding : Binding Key Value) : Key := Binding.key binding;
 
-value {A B} : Binding A B -> B
-  | (binding _ b) := b;
+value {Key Value} (binding : Binding Key Value) : Value := Binding.value binding;
 
-toPair {A B} : Binding A B -> Pair A B
-  | (binding a b) := a, b;
+toPair {Key Value} (binding : Binding Key Value) : Pair Key Value := key binding, value binding;
 
 instance
-bindingKeyOrdering {A B} {{Ord A}} : Ord (Binding A B) :=
-  mkOrd λ {b1 b2 := Ord.cmp (key b1) (key b2)};
+bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) :=
+  mkOrd@{
+    cmp (b1 b2 : Binding Key Value) : Ordering := Ord.cmp (key b1) (key b2)
+  };
 
-type Map A B := mkMap (AVLTree (Binding A B));
+type Map Key Value := mkMap (AVLTree (Binding Key Value));
 
-empty {A B} : Map A B := mkMap AVL.empty;
+empty {Key Value} : Map Key Value := mkMap AVL.empty;
 
 {-# specialize: [1, f] #-}
-insertWith {A B} {{Ord A}} (f : B -> B -> B) (k : A) (v : B) : Map A B -> Map A B
-  | (mkMap s) :=
-    let
-      f' : Binding A B -> Binding A B -> Binding A B
-        | (binding a b1) (binding _ b2) := binding a (f b1 b2);
-    in mkMap (Set.insertWith f' (binding k v) s);
+insertWith
+  {Key Value}
+  {{Ord Key}}
+  (fun : Value -> Value -> Value)
+  (key : Key)
+  (value : Value)
+  (map : Map Key Value)
+  : Map Key Value :=
+  case map of
+    mkMap tree :=
+      let
+        fun' (binding1 binding2 : Binding Key Value) : Binding Key Value :=
+          case binding1, binding2 of mkBinding a b1, mkBinding _ b2 := mkBinding a (fun b1 b2);
+        binding := mkBinding key value;
+      in mkMap (Set.insertWith fun' binding tree);
 
 insert {A B : Type} {{Ord A}} : A -> B -> Map A B -> Map A B := insertWith λ {old new := new};
 
diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
index 095171ad..d02e565f 100644
--- a/Stdlib/Data/Maybe.juvix
+++ b/Stdlib/Data/Maybe.juvix
@@ -11,35 +11,39 @@ import Stdlib.Trait.Monad open;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
+import Stdlib.Data.Pair.Base open;
 
 {-# specialize: true, inline: case #-}
 instance
 eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
-  mkEq
-    λ {
-      | nothing nothing := true
-      | (just a1) (just a2) := Eq.eq a1 a2
-      | _ _ := false
-    };
+  mkEq@{
+    eq (m1 m2 : Maybe A) : Bool :=
+      case m1, m2 of
+        | nothing, nothing := true
+        | just a1, just a2 := Eq.eq a1 a2
+        | _ := false
+  };
 
 instance
 showMaybeI {A} {{Show A}} : Show (Maybe A) :=
-  mkShow
-    λ {
-      | nothing := "nothing"
-      | (just a) := "just " ++str Show.show a
-    };
+  mkShow@{
+    show (m : Maybe A) : String :=
+      case m of
+        | nothing := "nothing"
+        | just a := "just " ++str Show.show a
+  };
 
 {-# specialize: true, inline: case #-}
 instance
 ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
-  mkOrd
-    λ {
-      | nothing nothing := EQ
-      | (just a1) (just a2) := Ord.cmp a1 a2
-      | nothing (just _) := LT
-      | (just _) nothing := GT
-    };
+  mkOrd@{
+    cmp (m1 m2 : Maybe A) : Ordering :=
+      case m1, m2 of
+        | nothing, nothing := Equal
+        | just a1, just a2 := Ord.cmp a1 a2
+        | nothing, just _ := LessThan
+        | just _, nothing := GreaterThan
+  };
 
 {-# specialize: true, inline: case #-}
 instance
@@ -58,15 +62,17 @@ instance
 applicativeMaybeI : Applicative Maybe :=
   mkApplicative@{
     pure := just;
-    ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
-      | (just f) (just x) := just (f x)
-      | _ _ := nothing
+    ap {A B} (listOfFuns : Maybe (A -> B)) (list : Maybe A) : Maybe B :=
+      case listOfFuns, list of
+        | just f, just x := just (f x)
+        | _, _ := nothing
   };
 
 instance
 monadMaybeI : Monad Maybe :=
   mkMonad@{
-    bind {A B} : Maybe A -> (A -> Maybe B) -> Maybe B
-      | nothing _ := nothing
-      | (just a) f := f a
+    bind {A B} (maybe : Maybe A) (fun : A -> Maybe B) : Maybe B :=
+      case maybe of
+        | nothing := nothing
+        | just a := fun a
   };
diff --git a/Stdlib/Data/Maybe/Base.juvix b/Stdlib/Data/Maybe/Base.juvix
index 390226d3..a35c60c1 100644
--- a/Stdlib/Data/Maybe/Base.juvix
+++ b/Stdlib/Data/Maybe/Base.juvix
@@ -5,17 +5,20 @@ import Juvix.Builtin.V1.Bool open;
 
 --- Extracts the value from a ;Maybe; if present, else returns the given value.
 {-# inline: true #-}
-fromMaybe {A} (a : A) : Maybe A → A
-  | nothing := a
-  | (just a) := a;
+fromMaybe {A} (defaultValue : A) (maybeValue : Maybe A) : A :=
+  case maybeValue of
+    | nothing := defaultValue
+    | just a := a;
 
 --- Applies a function to the value from a ;Maybe; if present, else returns the
 --- given value.
 {-# inline: true, isabelle-function: {name: "case_option"} #-}
-maybe {A B} (b : B) (f : A → B) : Maybe A → B
-  | nothing := b
-  | (just a) := f a;
+maybe {A B} (defaultValue : B) (fun : A -> B) (maybeValue : Maybe A) : B :=
+  case maybeValue of
+    | nothing := defaultValue
+    | just a := fun a;
 
-isJust {A} : Maybe A -> Bool
-  | nothing := false
-  | (just _) := true;
+isJust {A} (maybeValue : Maybe A) : Bool :=
+  case maybeValue of
+    | nothing := false
+    | just _ := true;
diff --git a/Stdlib/Data/Nat/Ord.juvix b/Stdlib/Data/Nat/Ord.juvix
index c97c6290..61b439f8 100644
--- a/Stdlib/Data/Nat/Ord.juvix
+++ b/Stdlib/Data/Nat/Ord.juvix
@@ -3,14 +3,14 @@ module Stdlib.Data.Nat.Ord;
 import Stdlib.Data.Fixity open;
 
 import Stdlib.Data.Nat.Base open;
-import Stdlib.Trait.Ord open using {EQ; LT; GT; Ordering};
+import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering};
 import Stdlib.Data.Bool.Base open;
 
 syntax operator == comparison;
 
 --- Tests for equality.
 builtin nat-eq
-== : Nat → Nat → Bool
+== : Nat -> Nat -> Bool
   | zero zero := true
   | zero _ := false
   | _ zero := false
@@ -25,7 +25,7 @@ syntax operator <= comparison;
 
 --- Returns ;true; iff the first element is less than or equal to the second.
 builtin nat-le
-<= : Nat → Nat → Bool
+<= : Nat -> Nat -> Bool
   | zero _ := true
   | _ zero := false
   | (suc n) (suc m) := n <= m;
@@ -50,12 +50,18 @@ syntax operator >= comparison;
 {-# inline: true #-}
 compare (n m : Nat) : Ordering :=
   if
-    | n == m := EQ
-    | n < m := LT
-    | else := GT;
+    | n == m := Equal
+    | n < m := LessThan
+    | else := GreaterThan;
 
 --- Returns the smaller ;Nat;.
-min (x y : Nat) : Nat := ite (x < y) x y;
+min (x y : Nat) : Nat :=
+  if
+    | x < y := x
+    | else := y;
 
 --- Returns the larger ;Nat;.
-max (x y : Nat) : Nat := ite (x > y) x y;
+max (x y : Nat) : Nat :=
+  if
+    | x > y := x
+    | else := y;
diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix
index 6ddf5275..feb2a550 100644
--- a/Stdlib/Data/Pair.juvix
+++ b/Stdlib/Data/Pair.juvix
@@ -11,20 +11,29 @@ import Stdlib.Trait.Show open;
 {-# specialize: true, inline: case #-}
 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 eqA}} {{mkEq eqB}} :=
+    mkEq@{
+      eq (p1 p2 : Pair A B) : Bool := case p1, p2 of (a1, b1), a2, b2 := eqA a1 a2 && eqB b1 b2
+    };
 
 {-# specialize: true, inline: case #-}
 instance
 ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
-  | {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=
-    mkOrd
-      λ {(a1, b1) (a2, b2) :=
-        case cmp-a a1 a2 of
-          | LT := LT
-          | GT := GT
-          | EQ := cmp-b b1 b2};
+  | {{mkOrd cmpA}} {{mkOrd cmpB}} :=
+    mkOrd@{
+      cmp (p1 p2 : Pair A B) : Ordering :=
+        case p1, p2 of
+          (a1, b1), a2, b2 :=
+            case cmpA a1 a2 of
+              | LessThan := LessThan
+              | GreaterThan := GreaterThan
+              | Equal := cmpB b1 b2
+    };
 
 instance
 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 showA}} {{mkShow showB}} :=
+    mkShow@{
+      show (p : Pair A B) : String :=
+        case p of a, b := "(" ++str showA a ++str " , " ++str showB b ++str ")"
+    };
diff --git a/Stdlib/Data/Pair/Base.juvix b/Stdlib/Data/Pair/Base.juvix
index 07ea8405..39a41eeb 100644
--- a/Stdlib/Data/Pair/Base.juvix
+++ b/Stdlib/Data/Pair/Base.juvix
@@ -8,33 +8,26 @@ syntax operator , pair;
 builtin pair
 type Pair (A B : Type) := , : A → B → Pair A B;
 
---- Converts a function of two arguments to a function with a product argument.
-uncurry {A B C} (f : A -> B -> C) : Pair A B -> C
-  | (a, b) := f a b;
+--- Converts a function f of two arguments to a function with a product argument.
+uncurry {A B C} (f : A -> B -> C) (pair : Pair A B) : C := case pair of a, b := f a b;
 
---- Converts a function with a product argument to a function of two arguments.
+--- Converts a function f 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);
 
 --- Projects the first component of a tuple.
-fst {A B} : Pair A B → A
-  | (a, _) := a;
+fst {A B} (pair : Pair A B) : A := case pair of a, _ := a;
 
 --- Projects the second component of a tuple.
-snd {A B} : Pair A B → B
-  | (_, b) := b;
+snd {A B} (pair : Pair A B) : B := case pair of _, b := b;
 
 --- Swaps the components of a tuple.
-swap {A B} : Pair A B → Pair B A
-  | (a, b) := b, a;
+swap {A B} (pair : Pair A B) : Pair B A := case pair of a, b := b, a;
 
---- Applies a function to the first component.
-first {A B A'} (f : A → A') : Pair A B → Pair A' B
-  | (a, b) := f a, b;
+--- Applies a function f to the first component.
+first {A B A'} (f : A -> A') (pair : Pair A B) : Pair A' B := case pair of a, b := f a, b;
 
---- Applies a function to the second component.
-second {A B B'} (f : B → B') : Pair A B → Pair A B'
-  | (a, b) := a, f b;
+--- Applies a function f to the second component.
+second {A B B'} (f : B -> B') (pair : Pair A B) : Pair A B' := case pair of a, b := a, f b;
 
---- Applies a function to both components.
-both {A B} (f : A → B) : Pair A A → Pair B B
-  | (a, b) := f a, f b;
+--- Applies a function f to both components.
+both {A B} (f : A -> B) (pair : Pair A A) : Pair B B := case pair of a, b := f a, f b;
diff --git a/Stdlib/Data/Queue/Base.juvix b/Stdlib/Data/Queue/Base.juvix
index 1b715f38..b6085e95 100644
--- a/Stdlib/Data/Queue/Base.juvix
+++ b/Stdlib/Data/Queue/Base.juvix
@@ -18,58 +18,66 @@ import Stdlib.Function open;
 import Stdlib.Trait.Foldable open;
 
 --- A first-in-first-out data structure
-type Queue (A : Type) := queue (List A) (List A);
+type Queue (A : Type) :=
+  mkQueue {
+    front : List A;
+    back : List A
+  };
 
 --- 𝒪(1). The empty ;Queue;.
-empty {A} : Queue A := queue nil nil;
+empty {A} : Queue A := mkQueue nil nil;
 
 --- 𝒪(1). Returns ;true; when the ;Queue; has no elements.
-isEmpty {A} : Queue A -> Bool
-  | (queue nil nil) := true
-  | _ := false;
+isEmpty {A} (queue : Queue A) : Bool :=
+  case queue of
+    | mkQueue nil nil := true
+    | _ := false;
 
 --- 𝒪(1). Returns first element of the ;Queue;, if any.
-head {A} : Queue A -> Maybe A
-  | (queue nil _) := nothing
-  | (queue (x :: _) _) := just x;
+head {A} (queue : Queue A) : Maybe A :=
+  case queue of
+    | mkQueue nil _ := nothing
+    | mkQueue (x :: _) _ := just x;
 
 --- 𝒪(1). Removes the first element from the ;Queue;. If the ;Queue; is empty
 --  then returns ;nothing;.
-tail {A} : Queue A -> Maybe (Queue A)
-  | (queue nil _) := nothing
-  | (queue (_ :: front) back) := just (queue front back);
+tail {A} (queue : Queue A) : Maybe (Queue A) :=
+  case queue of
+    | mkQueue nil _ := nothing
+    | mkQueue (_ :: front) back := just (mkQueue front back);
 
 --- 𝒪(n) worst-case, but 𝒪(1) amortized
 {-# inline: true #-}
-check {A} : Queue A -> Queue A
-  | (queue nil back) := queue (reverse back) nil
-  | q := q;
+check {A} (queue : Queue A) : Queue A :=
+  case queue of
+    | mkQueue nil back := mkQueue (reverse back) nil
+    | q := q;
 
 --- 𝒪(n) worst-case, but 𝒪(1) amortized. Returns the first element and the
 --  rest of the ;Queue;. If the ;Queue; is empty then returns ;nothing;.
-pop {A} : Queue A -> Maybe (Pair A (Queue A))
-  | (queue nil _) := nothing
-  | (queue (x :: front) back) := just (x, check (queue front back));
+pop {A} (queue : Queue A) : Maybe (Pair A (Queue A)) :=
+  case queue of
+    | mkQueue nil _ := nothing
+    | mkQueue (x :: front) back := just (x, check (mkQueue front back));
 
 --- 𝒪(1). Adds an element to the end of the ;Queue;.
-push {A} (x : A) : Queue A -> Queue A
-  | (queue front back) := check (queue front (x :: back));
+push {A} (x : A) (queue : Queue A) : Queue A :=
+  case queue of mkQueue front back := check (mkQueue front (x :: back));
 
 --- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
-pushMany {A} (xs : List A) (q : Queue A) : Queue A := for (acc := q) (x in xs) push x acc;
+pushMany {A} (list : List A) (queue : Queue A) : Queue A :=
+  for (acc := queue) (x in list) {push x acc};
 
 --- 𝒪(n). Build a ;Queue; from a ;List;.
-fromList {A} (xs : List A) : Queue A := pushMany xs empty;
+fromList {A} (list : List A) : Queue A := pushMany list empty;
 
 --- toList: O(n). Returns a ;List; of the elements in the ;Queue;.
 --- The elements are in the same order as they appear in the ;Queue;
 --- (i.e. the first element of the ;Queue; is the first element of the ;List;).
-toList {A} : Queue A -> List A
-  | (queue front back) := front ++ reverse back;
+toList {A} (queue : Queue A) : List A := case queue of mkQueue front back := front ++ reverse back;
 
 --- 𝒪(n). Returns the number of elements in the ;Queue;.
-size {A} : Queue A -> Nat
-  | (queue front back) := length front + length back;
+size {A} (queue : Queue A) : Nat := case queue of mkQueue front back := length front + length back;
 
 instance
 eqQueueI {A} {{Eq A}} : Eq (Queue A) := mkEq ((==) on toList);
diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
index b70ad273..f847cea5 100644
--- a/Stdlib/Data/Range.juvix
+++ b/Stdlib/Data/Range.juvix
@@ -25,13 +25,13 @@ syntax operator to range;
 
 --- `x to y` is the range [x..y]
 {-# inline: always #-}
-to {N} {{Natural N}} (l h : N) : Range N := mkRange l h;
+to {N} {{Natural N}} (low high : N) : Range N := mkRange low high;
 
 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) : StepRange N := mkStepRange r s;
+step {N} (range : Range N) (stp : N) : StepRange N := mkStepRange range stp;
 
 -- This instance assumes that `low <= high`.
 {-# specialize: true, inline: case #-}
@@ -39,7 +39,7 @@ instance
 foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
   mkFoldable@{
     {-# specialize: [1, 3] #-}
-    for {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
+    for {B : Type} (f : B -> N -> B) (initialValue : B) : Range N -> B
       | (mkRange low high) :=
         let
           {-# specialize-by: [f, high] #-}
@@ -48,16 +48,16 @@ foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
             if
               | next == high := f acc next
               | else := go (f acc next) (next + 1);
-        in go ini low;
+        in go initialValue low;
     {-# specialize: [1, 3] #-}
-    rfor {B : Type} (f : B -> N -> B) (ini : B) : Range N -> B
+    rfor {B : Type} (f : B -> N -> B) (initialValue : B) : Range N -> B
       | (mkRange low high) :=
         let
           {-# specialize-by: [f, high] #-}
           terminating
           go (next : N) : B :=
             if
-              | next == high := f ini next
+              | next == high := f initialValue next
               | else := f (go (next + 1)) next;
         in go low
   };
@@ -68,7 +68,7 @@ instance
 foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
   mkFoldable@{
     {-# specialize: [1, 3] #-}
-    for {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
+    for {B : Type} (f : B -> N -> B) (initialValue : B) : StepRange N -> B
       | (mkStepRange (mkRange low high) step) :=
         let
           {-# specialize-by: [f, high, step] #-}
@@ -77,9 +77,9 @@ foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
             if
               | next > high := acc
               | else := go (f acc next) (next + step);
-        in go ini low;
+        in go initialValue low;
     {-# specialize: [1, 3] #-}
-    rfor {B : Type} (f : B -> N -> B) (ini : B) : StepRange N -> B
+    rfor {B : Type} (f : B -> N -> B) (initialValue : B) : StepRange N -> B
       | (mkStepRange (mkRange low high) step) :=
         let
           {-# specialize-by: [f, high, step] #-}
@@ -87,6 +87,6 @@ foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
           go (next : N) : B :=
             if
               | next <= high := f (go (next + step)) next
-              | else := ini;
+              | else := initialValue;
         in go low
   };
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index 98b301f6..59430367 100644
--- a/Stdlib/Data/Result.juvix
+++ b/Stdlib/Data/Result.juvix
@@ -3,6 +3,7 @@ module Stdlib.Data.Result;
 import Stdlib.Data.Result.Base open public;
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
+import Stdlib.Data.Pair.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
@@ -11,59 +12,63 @@ import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
 instance
-ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
+ordResultI {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) :=
   mkOrd@{
-    cmp : Result A B -> Result A B -> Ordering
-      | (error a1) (error a2) := Ord.cmp a1 a2
-      | (ok b1) (ok b2) := Ord.cmp b1 b2
-      | (error _) (ok _) := LT
-      | (ok _) (error _) := GT
+    cmp (result1 result2 : Result Error Value) : Ordering :=
+      case result1, result2 of
+        | error a1, error a2 := Ord.cmp a1 a2
+        | ok b1, ok b2 := Ord.cmp b1 b2
+        | error _, ok _ := LessThan
+        | ok _, error _ := GreaterThan
   };
 
 {-# specialize: true, inline: case #-}
 instance
-eqResultI {A B} {{Eq A}} {{Eq B}} : Eq (Result A B) :=
+eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) :=
   mkEq@{
-    eq : Result A B -> Result A B -> Bool
-      | (error a1) (error a2) := a1 == a2
-      | (ok b1) (ok b2) := b1 == b2
-      | _ _ := false
+    eq (result1 result2 : Result Error Value) : Bool :=
+      case result1, result2 of
+        | error a1, error a2 := a1 == a2
+        | ok b1, ok b2 := b1 == b2
+        | _, _ := false
   };
 
 instance
-showResultI {A B} {{Show A}} {{Show B}} : Show (Result A B) :=
+showResultI {Error Value} {{Show Error}} {{Show Value}} : Show (Result Error Value) :=
   mkShow@{
-    show : Result A B -> String
+    show : Result Error Value -> String
       | (error x) := "Error (" ++str Show.show x ++str ")"
       | (ok x) := "Ok (" ++str Show.show x ++str ")"
   };
 
 {-# specialize: true, inline: case #-}
 instance
-functorResultI {err} : Functor (Result err) :=
+functorResultI {Error} : Functor (Result Error) :=
   mkFunctor@{
     map := mapOk
   };
 
 {-# specialize: true, inline: true #-}
 instance
-monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res :=
+monomorphicFunctorResultI {Error Value} : Monomorphic.Functor (Result Error Value) Value :=
   fromPolymorphicFunctor;
 
 instance
-applicativeResultI {err} : Applicative (Result err) :=
+applicativeResultI {Error} : Applicative (Result Error) :=
   mkApplicative@{
     pure := ok;
-    ap {A B} : Result err (A -> B) -> Result err A -> Result err B
-      | (ok f) (ok x) := ok (f x)
-      | (ok _) (error e) := error e
-      | (error e) _ := error e
+    ap {A B} (resultFun : Result Error (A -> B)) (result : Result Error A) : Result Error B :=
+      case resultFun, result of
+        | ok f, ok x := ok (f x)
+        | ok _, error e := error e
+        | error e, _ := error e
   };
 
 instance
-monadResultI {err} : Monad (Result err) :=
+monadResultI {Error} : Monad (Result Error) :=
   mkMonad@{
-    bind {A B} : Result err A -> (A -> Result err B) -> Result err B
-      | (error e) _ := error e
-      | (ok a) f := f a
+    bind {A B} (result : Result Error A) (fun : A -> Result Error B) : Result Error B :=
+      case result of
+        | error e := error e
+        | ok a := fun a
   };
diff --git a/Stdlib/Data/Result/Base.juvix b/Stdlib/Data/Result/Base.juvix
index b0a65c65..3d98ffe3 100644
--- a/Stdlib/Data/Result/Base.juvix
+++ b/Stdlib/Data/Result/Base.juvix
@@ -6,46 +6,68 @@ import Stdlib.Function open;
 
 --- The Result type represents either a success with a value of `ok` or an error
 --- with value `error`.
-type Result E A :=
-  | error E
-  | ok A;
+type Result Error Value :=
+  | error Error
+  | ok Value;
 
 --- 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
-  | (error a) := onError a
-  | (ok a) := onOk a;
+{-# inline: true #-}
+handleResult
+  {Error Value1 Value2}
+  (onError : Error -> Value2)
+  (onOk : Value1 -> Value2)
+  (result : Result Error Value1)
+  : Value2 :=
+  case result of
+    | 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;
+--- Apply a function f to the ;error; value of a Result.
+mapError
+  {Value Error1 Error2}
+  (f : Error1 -> Error2)
+  (result : Result Error1 Value)
+  : Result Error2 Value := handleResult (f >> error) ok result;
 
---- 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);
+--- Apply a function f to the ;ok; value of a Result.
+mapOk
+  {Error Value1 Value2}
+  (f : Value1 -> Value2)
+  (result : Result Error Value1)
+  : Result Error Value2 := handleResult error (f >> ok) result;
 
 --- Return ;true; if the value is an ;error;, otherwise ;false;.
-isError {E A} : Result E A -> Bool
-  | (error _) := true
-  | (ok _) := false;
+isError {Error Value} (result : Result Error Value) : Bool :=
+  case result of
+    | error _ := true
+    | ok _ := false;
 
 --- Return ;true; if the value is ;ok;, otherwise ;false;.
-isOk {E A} : Result E A -> Bool
-  | (error _) := false
-  | (ok _) := true;
+isOk {Error Value} (result : Result Error Value) : Bool :=
+  case result of
+    | error _ := false
+    | ok _ := true;
 
---- Return the contents of an ;error; value, otherwise return a default.
-fromError {E A} (default : E) : Result E A -> E
-  | (error a) := a
-  | (ok _) := default;
+--- Return the contents of an ;error; value, otherwise return defaultError.
+fromError {Error Value} (defaultError : Error) (result : Result Error Value) : Error :=
+  case result of
+    | error a := a
+    | ok _ := defaultError;
 
---- Return the contents of an ;ok; value, otherwise return a default.
-fromOk {E A} (default : A) : Result E A -> A
-  | (error _) := default
-  | (ok b) := b;
+--- Return the contents of an ;ok; value, otherwise return defaultValue.
+fromOk {Error Value} (defaultValue : Value) (result : Result Error Value) : Value :=
+  case result of
+    | error _ := defaultValue
+    | 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 {Error Value} (result : Result Error Value) : Maybe Value :=
+  handleResult (const nothing) just result;
 
 --- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`.
-maybeToResult {E A} (defaultError : E) : Maybe A -> Result E A
-  | nothing := error defaultError
-  | (just x) := ok x;
+maybeToResult
+  {Error Value} (defaultError : Error) (maybeValue : Maybe Value) : Result Error Value :=
+  case maybeValue of
+    | nothing := error defaultError
+    | just x := ok x;
diff --git a/Stdlib/Data/Set/AVL.juvix b/Stdlib/Data/Set/AVL.juvix
index 988bd507..a4b37d8b 100644
--- a/Stdlib/Data/Set/AVL.juvix
+++ b/Stdlib/Data/Set/AVL.juvix
@@ -14,7 +14,7 @@ import Stdlib.Data.Nat open;
 import Stdlib.Data.Int open;
 import Stdlib.Data.Bool open;
 import Stdlib.Data.Pair open;
-import Stdlib.Data.List open;
+import Stdlib.Data.List open hiding {isMember};
 import Stdlib.Data.String open;
 import Stdlib.Trait.Foldable open;
 import Stdlib.Function open;
@@ -24,138 +24,168 @@ type AVLTree (A : Type) :=
   | --- An empty AVL tree.
     empty
   | --- A node of an AVL tree.
-    node A Nat (AVLTree A) (AVLTree A);
+    node {
+      element : A;
+      height : Nat;
+      left : AVLTree A;
+      right : AVLTree A
+    };
 
 --- 𝒪(1) Retrieves the height of an ;AVLTree;. The height is the distance from
 --- the root to the deepest child.
-height {A} : AVLTree A -> Nat
-  | empty := 0
-  | (node _ h _ _) := h;
+height {A} (tree : AVLTree A) : Nat :=
+  case tree of
+    | empty := 0
+    | node@{height} := height;
 
 type BalanceFactor :=
-  | --- Left children is higher.
+  | --- Left child is higher.
     LeanLeft
   | --- Equal heights of children.
     LeanNone
-  | --- Right children is higher.
+  | --- Right child is higher.
     LeanRight;
 
-{-# inline: true #-}
-diffFactor {A} : AVLTree A -> Int
-  | empty := 0
-  | (node _ _ left right) := intSubNat (height right) (height left);
+diffFactor {A} (tree : AVLTree A) : Int :=
+  case tree of
+    | empty := 0
+    | node@{left; right} := intSubNat (height right) (height left);
 
---- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree
---- minus the height of the left subtree.
 {-# inline: true #-}
-balanceFactor {A} (t : AVLTree A) : BalanceFactor :=
+balanceFactor' {A} (left right : AVLTree A) : BalanceFactor :=
   let
-    diff : Int := diffFactor t;
+    h1 := height left;
+    h2 := height right;
   in if
-    | 0 < diff := LeanRight
-    | diff < 0 := LeanLeft
+    | h1 < h2 := LeanRight
+    | h2 < h1 := LeanLeft
     | else := LeanNone;
 
+--- 𝒪(1). Computes the balance factor, i.e., the height of the right subtree
+--- minus the height of the left subtree.
+balanceFactor {A} (tree : AVLTree A) : BalanceFactor :=
+  -- We avoid `diffFactor` here for efficiency.
+  case tree of
+    | empty := LeanNone
+    | node@{left; right} := balanceFactor' left right;
+
 --- 𝒪(1). Helper function for creating a node.
-mknode {A} (val : A) (l : AVLTree A) (r : AVLTree A) : AVLTree A :=
-  node val (1 + max (height l) (height r)) l r;
+mkNode {A} (value : A) (left : AVLTree A) (right : AVLTree A) : AVLTree A :=
+  node value (1 + max (height left) (height right)) left right;
 
 --- 𝒪(1). Left rotation.
-rotateLeft {A} : AVLTree A -> AVLTree A
-  | (node x _ a (node z _ b c)) := mknode z (mknode x a b) c
-  | n := n;
+rotateLeft {A} (tree : AVLTree A) : AVLTree A :=
+  case tree of
+    | node x _ a (node z _ b c) := mkNode z (mkNode x a b) c
+    | n := n;
 
 --- 𝒪(1). Right rotation.
-rotateRight {A} : AVLTree A -> AVLTree A
-  | (node z _ (node y _ x t3) t4) := mknode y x (mknode z t3 t4)
-  | n := n;
+rotateRight {A} (tree : AVLTree A) : AVLTree A :=
+  case tree of
+    | node z _ (node y _ x t3) t4 := mkNode y x (mkNode z t3 t4)
+    | n := n;
 
 --- 𝒪(1). Applies local rotations if needed.
-balance : {A : Type} -> AVLTree A -> AVLTree A
-  | empty := empty
-  | n@(node x h l r) :=
-    let
-      factor : BalanceFactor := balanceFactor n;
-    in case factor of
-         | LeanRight :=
-           case balanceFactor r of {
-             | LeanLeft := rotateLeft (mknode x l (rotateRight r))
-             | _ := rotateLeft n
-           }
-         | LeanLeft :=
-           case balanceFactor l of {
-             | LeanRight := rotateRight (mknode x (rotateLeft l) r)
-             | _ := rotateRight n
-           }
-         | LeanNone := n;
+balance {A} (tree : AVLTree A) : AVLTree A :=
+  case tree of
+    | empty := empty
+    | node@{element; height; left; right} :=
+      case balanceFactor' left right of
+        | LeanRight :=
+          case balanceFactor right of {
+            | LeanLeft := rotateLeft (mkNode element left (rotateRight right))
+            | _ := rotateLeft tree
+          }
+        | LeanLeft :=
+          case balanceFactor left of {
+            | LeanRight := rotateRight (mkNode element (rotateLeft left) right)
+            | _ := rotateRight tree
+          }
+        | LeanNone := tree;
 
 --- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function.
---- Ord A, Ord K and f must be compatible. i.e cmp_k (f a1) (f a2) == cmp_a a1 a2
-lookupWith {A K} {{o : Ord K}} (f : A -> K) (x : K) : AVLTree A -> Maybe A :=
+--- Ord A, Ord K and fun must be compatible. i.e cmp_k (fun a1) (fun a2) == cmp_a a1 a2
+{-# specialize: [1, 2] #-}
+lookupWith {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (tree : AVLTree A) : Maybe A :=
   let
-    {-# specialize-by: [o, f] #-}
+    {-# specialize-by: [order, fun] #-}
     go : AVLTree A -> Maybe A
       | empty := nothing
-      | m@(node y h l r) :=
-        case Ord.cmp x (f y) of
-          | LT := go l
-          | GT := go r
-          | EQ := just y;
-  in go;
+      | node@{element; left; right} :=
+        case Ord.cmp elem (fun element) of
+          | LessThan := go left
+          | GreaterThan := go right
+          | Equal := just element;
+  in go tree;
 
 --- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
 {-# specialize: [1] #-}
-member? {A} {{Ord A}} (x : A) : AVLTree A -> Bool := lookupWith id x >> isJust;
+lookup {A} {{Ord A}} (elem : A) (tree : AVLTree A) : Maybe A := lookupWith id elem tree;
 
---- 𝒪(log 𝓃). Inserts an element into and ;AVLTree; using a function to
+--- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
+isMember {A} {{Ord A}} (elem : A) (tree : AVLTree A) : Bool := isJust (lookupWith id elem tree);
+
+--- 𝒪(log 𝓃). Inserts an element elem into and ;AVLTree; using a function to
 --- deduplicate entries.
 ---
---- Assumption: Given a1 == a2 then f a1 a2 == a1 == a2
+--- Assumption: If a1 == a2 then fun a1 a2 == a1 == a2
 --- where == comes from Ord a.
-insertWith {A} {{o : Ord A}} (f : A -> A -> A) (x : A) : AVLTree A -> AVLTree A :=
+{-# specialize: [1, 2] #-}
+insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (tree : AVLTree A) : AVLTree A :=
   let
-    {-# specialize-by: [o, f] #-}
+    {-# specialize-by: [order, fun] #-}
     go : AVLTree A -> AVLTree A
-      | empty := mknode x empty empty
-      | m@(node y h l r) :=
-        case Ord.cmp x y of
-          | LT := balance (mknode y (go l) r)
-          | GT := balance (mknode y l (go r))
-          | EQ := node (f y x) h l r;
-  in go;
+      | empty := mkNode elem empty empty
+      | node@{element; height; left; right} :=
+        case Ord.cmp elem element of
+          | LessThan := balance (mkNode element (go left) right)
+          | GreaterThan := balance (mkNode element left (go right))
+          | Equal := node (fun element elem) height left right;
+  in go tree;
 
 --- 𝒪(log 𝓃). Inserts an element into and ;AVLTree;.
-insert {A} {{Ord A}} : A -> AVLTree A -> AVLTree A := insertWith (flip const);
+insert {A} {{Ord A}} (elem : A) (tree : AVLTree A) : AVLTree A := insertWith (flip const) elem tree;
+
+--- 𝒪(log 𝓃). Removes the minimum element from an ;AVLTree;.
+{-# specialize: [1] #-}
+deleteMin {A} {{Ord A}} : (tree : AVLTree A) -> Maybe (Pair A (AVLTree A))
+  | empty := nothing
+  | node@{element; left; right} :=
+    case deleteMin left of
+      | nothing := just (element, right)
+      | just (element', left') := just (element', mkNode element left' right);
 
 --- 𝒪(log 𝓃). Removes an element from an ;AVLTree; based on a projected comparison value.
 ---
---- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2)
-deleteWith {A B} {{o : Ord A}} {{po : Ord B}} (p : A -> B) (x : B) : AVLTree A -> AVLTree A :=
+--- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (fun a1 == fun a2) == (a1 == a2)
+{-# specialize: [1, 2, 3] #-}
+deleteWith
+  {A B}
+  {{orderA : Ord A}}
+  {{orderB : Ord B}}
+  (fun : A -> B)
+  (elem : B)
+  (tree : AVLTree A)
+  : AVLTree A :=
   let
-    {-# specialize-by: [o, po, p] #-}
-    deleteMin : AVLTree A -> Maybe (Pair A (AVLTree A))
-      | empty := nothing
-      | (node v _ l r) :=
-        case deleteMin l of
-          | nothing := just (v, r)
-          | just (m, l') := just (m, mknode v l' r);
-    {-# specialize-by: [o, po, p] #-}
+    {-# specialize-by: [orderA, orderB, fun] #-}
     go : AVLTree A -> AVLTree A
       | empty := empty
-      | (node y h l r) :=
-        case Ord.cmp x (p y) of
-          | LT := balance (mknode y (go l) r)
-          | GT := balance (mknode y l (go r))
-          | EQ :=
-            case l of
-              | empty := r
+      | node@{element; left; right} :=
+        case Ord.cmp elem (fun element) of
+          | LessThan := balance (mkNode element (go left) right)
+          | GreaterThan := balance (mkNode element left (go right))
+          | Equal :=
+            case left of
+              | empty := right
               | _ :=
-                case deleteMin r of
-                  | nothing := l
-                  | just (minRight, r') := balance (mknode minRight l r');
-  in go;
+                case deleteMin right of
+                  | nothing := left
+                  | just (minRight, right') := balance (mkNode minRight left right');
+  in go tree;
 
 --- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
+{-# specialize: [1] #-}
 delete {A} {{o : Ord A}} : A -> AVLTree A -> AVLTree A := deleteWith id;
 
 --- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;.
@@ -172,73 +202,78 @@ lookupMax {A} : AVLTree A -> Maybe A
   | (node _ _ l empty) := lookupMax l
   | (node _ _ _ r) := lookupMax r;
 
---- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree;.
+--- 𝒪(𝒹 log 𝓃). Deletes elements from an ;AVLTree;.
 {-# specialize: [1] #-}
 deleteMany {A} {{Ord A}} : List A -> AVLTree A -> AVLTree A := deleteManyWith id;
 
---- 𝒪(𝒹 log 𝓃). Deletes d elements from an ;AVLTree; based on a projected comparison value.
+--- 𝒪(𝒹 log 𝓃). Deletes elements from an ;AVLTree; based on a projected comparison value.
 ---
---- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (p a1 == p a2) == (a1 == a2)
-{-# specialize: [2] #-}
-deleteManyWith {A B} {{Ord A}} {{Ord B}} (p : A -> B) (d : List B) (t : AVLTree A) : AVLTree A :=
-  for (acc := t) (x in d)
-    deleteWith p x acc;
+--- Assumption: Ord A and Ord B are compatible, i.e., for a1 a2 in A, we have (fun a1 == fun a2) == (a1 == a2)
+{-# specialize: [1, 2] #-}
+deleteManyWith
+  {A B} {{Ord A}} {{Ord B}} (fun : A -> B) (toDelete : List B) (tree : AVLTree A) : AVLTree A :=
+  for (acc := tree) (x in toDelete) {deleteWith fun x acc};
 
 --- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that
 --- every two children do not differ on height by more than 1.
-isBalanced {A} : AVLTree A -> Bool
+isBalanced {A} : (tree : AVLTree A) -> Bool
   | empty := true
-  | n@(node _ _ l r) := isBalanced l && isBalanced r && abs (diffFactor n) <= 1;
+  | tree@node@{left; right} := isBalanced left && isBalanced right && abs (diffFactor tree) <= 1;
 
 --- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
 {-# specialize: [1] #-}
-fromList {A} {{Ord A}} (l : List A) : AVLTree A := for (acc := empty) (x in l) insert x acc;
+fromList {A} {{Ord A}} (list : List A) : AVLTree A := for (acc := empty) (x in list) {insert x acc};
 
 --- 𝒪(𝓃). Returns the number of elements of an ;AVLTree;.
 size {A} : AVLTree A -> Nat
   | empty := 0
-  | (node _ _ l r) := 1 + size l + size r;
+  | node@{left; right} := 1 + size left + size right;
 
---- 𝒪(𝓃). Returns the elements of an ;AVLTree; in ascending order.
+-- TODO: Implement this tail-recursively with an accumulator. Then it will be O(n).
+--- 𝒪(n log n). Returns the elements of an ;AVLTree; in ascending order.
 toList {A} : AVLTree A -> List A
   | empty := nil
-  | (node x _ l r) := toList l ++ (x :: nil) ++ toList r;
+  | node@{element; left; right} := toList left ++ (element :: nil) ++ toList right;
 
---- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of both ;AVLTree;s.
+-- TODO: avoid conversion to list.
+--- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of both ;AVLTree;s.
 intersection {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A :=
-  toList s1 |> filter \ {x := member? x s2} |> fromList;
+  toList s1 |> filter \ {x := isMember x s2} |> fromList;
 
---- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of the first but not the second ;AVLTree;.
+-- TODO: avoid conversion to list.
+--- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of the first but not the second ;AVLTree;.
 difference {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A :=
-  toList s1 |> filter \ {x := not (member? x s2)} |> fromList;
+  toList s1 |> filter \ {x := not (isMember x s2)} |> fromList;
 
---- 𝒪(𝓃). Returns an ;AVLTree; containing elements that are members of either the first or second ;AVLTree;.
+-- TODO: avoid conversion to list.
+--- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of either the first or second ;AVLTree;.
 union {A} {{Ord A}} (s1 s2 : AVLTree A) : AVLTree A := fromList (toList s1 ++ toList s2);
 
---- 𝒪(𝓃). Formats the tree in a debug friendly format.
-prettyDebug {A} {{Show A}} : AVLTree A -> String :=
+--- Formats the tree in a debug friendly format.
+prettyDebug {A} {{Show A}} (tree : AVLTree A) : String :=
   let
     go : AVLTree A -> String
       | empty := "_"
-      | n@(node v h l r) :=
+      | tree@node@{element; left; right} :=
         "("
-          ++str go l
+          ++str go left
           ++str " h"
-          ++str Show.show (diffFactor n)
+          ++str Show.show (diffFactor tree)
           ++str " "
-          ++str Show.show v
+          ++str Show.show element
           ++str " "
-          ++str go r
+          ++str go right
           ++str ")";
-  in go;
+  in go tree;
 
 --- 𝒪(𝓃).
-toTree {A} : AVLTree A -> Maybe (Tree A)
+toTree {A} : (tree : AVLTree A) -> Maybe (Tree A)
   | empty := nothing
-  | (node v _ l r) := just (Tree.node v (catMaybes (toTree l :: toTree r :: nil)));
+  | node@{element; left; right} :=
+    just (Tree.node element (catMaybes (toTree left :: toTree right :: nil)));
 
 --- Returns the textual representation of an ;AVLTree;.
-pretty {A} {{Show A}} : AVLTree A -> String := toTree >> maybe "empty" Tree.treeToString;
+pretty {A} {{Show A}} (tree : AVLTree A) : String := maybe "empty" Tree.treeToString (toTree tree);
 
 -- TODO: remove toList
 instance
@@ -248,16 +283,17 @@ eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) := mkEq ((==) on toList);
 instance
 ordAVLTreeI {A} {{Ord A}} : Ord (AVLTree A) := mkOrd (Ord.cmp on toList);
 
+-- TODO: remove toList
 {-# specialize: true, inline: case #-}
 instance
 polymorphicFoldableAVLTreeI : Polymorphic.Foldable AVLTree :=
   Polymorphic.mkFoldable@{
-    for {A B} (f : B -> A -> B) (acc : B) : AVLTree A -> B :=
-      toList >> Polymorphic.Foldable.for f acc;
-    rfor {A B} (f : B → A → B) (acc : B) : AVLTree A -> B :=
-      toList >> Polymorphic.Foldable.rfor f acc
+    for {A B} (f : B -> A -> B) (acc : B) (tree : AVLTree A) : B :=
+      Polymorphic.Foldable.for f acc (toList tree);
+    rfor {A B} (f : B → A → B) (acc : B) (tree : AVLTree A) : B :=
+      Polymorphic.Foldable.rfor f acc (toList tree)
   };
 
 {-# specialize: true, inline: true #-}
 instance
-foldableVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable;
+foldableAVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable;
diff --git a/Stdlib/Data/String/Base.juvix b/Stdlib/Data/String/Base.juvix
index ed81c3b2..a55090fc 100644
--- a/Stdlib/Data/String/Base.juvix
+++ b/Stdlib/Data/String/Base.juvix
@@ -6,7 +6,7 @@ import Stdlib.Function open;
 import Stdlib.Data.Fixity open;
 
 --- Concatenates a ;List; of ;String;s.
-concatStr : List String -> String := listFoldl (++str) "";
+concatStr (string : List String) : String := listFoldl (++str) "" string;
 
 --- Joins a ;List; of ;String;s with "\n".
-unlines : List String -> String := intersperse "\n" >> concatStr;
+unlines (list : List String) : String := concatStr (intersperse "\n" list);
diff --git a/Stdlib/Data/String/Ord.juvix b/Stdlib/Data/String/Ord.juvix
index 474795ec..af56de05 100644
--- a/Stdlib/Data/String/Ord.juvix
+++ b/Stdlib/Data/String/Ord.juvix
@@ -8,4 +8,4 @@ import Stdlib.Data.Bool open;
 syntax operator == comparison;
 --- Equality for ;String;s.
 builtin string-eq
-axiom == : String → String → Bool;
+axiom == : String -> String -> Bool;
diff --git a/Stdlib/Data/Tree.juvix b/Stdlib/Data/Tree.juvix
index c5e943f5..3756df8e 100644
--- a/Stdlib/Data/Tree.juvix
+++ b/Stdlib/Data/Tree.juvix
@@ -10,22 +10,26 @@ import Stdlib.Function open;
 Forest (A : Type) : Type := List (Tree A);
 
 --- N-Ary tree.
-positive
-type Tree (A : Type) := node A (List (Tree A));
-
-shift (first other : String) (xs : List String) : List String :=
-  zipWith (++str) (first :: replicate (length xs) other) xs;
+type Tree (A : Type) :=
+  node {
+    element : A;
+    children : List (Tree A)
+  };
 
 terminating
-draw {A} {{Show A}} : Tree A -> List String
-  | (node v cs) := Show.show v :: drawForest cs;
+draw {A} {{Show A}} (tree : Tree A) : List String :=
+  Show.show (Tree.element tree) :: drawForest (Tree.children tree);
 
 terminating
-drawForest {A} {{Show A}} : Forest A -> List String
-  | [] := []
-  | [h] := "|" :: shift "`- " "   " (draw h)
-  | (h :: hs) := "|" :: shift "+- " "|  " (draw h) ++ drawForest hs;
-
-treeToString {A} {{Show A}} : Tree A -> String := draw >> unlines;
-
-forestToString {A} {{Show A}} : Forest A -> String := drawForest >> unlines;
+drawForest {A} {{Show A}} (forest : Forest A) : List String :=
+  let
+    shift (first other : String) (xs : List String) : List String :=
+      zipWith (++str) (first :: replicate (length xs) other) xs;
+  in case forest of
+       | [] := []
+       | [h] := "|" :: shift "`- " "   " (draw h)
+       | h :: hs := "|" :: shift "+- " "|  " (draw h) ++ drawForest hs;
+
+treeToString {A} {{Show A}} (tree : Tree A) : String := unlines (draw tree);
+
+forestToString {A} {{Show A}} (forest : Forest A) : String := unlines (drawForest forest);
diff --git a/Stdlib/Data/UnbalancedSet.juvix b/Stdlib/Data/UnbalancedSet.juvix
index db420594..f1af8245 100644
--- a/Stdlib/Data/UnbalancedSet.juvix
+++ b/Stdlib/Data/UnbalancedSet.juvix
@@ -7,40 +7,46 @@ import Stdlib.Trait.Ord as Ord open using {Ord; mkOrd; module Ord};
 import Stdlib.Data.BinaryTree as Tree;
 open Tree using {BinaryTree; leaf; node};
 
-type UnbalancedSet (A : Type) := unbalancedSet : Ord A -> BinaryTree A -> UnbalancedSet A;
-
-empty {A} {{o : Ord A}} : UnbalancedSet A := unbalancedSet o leaf;
-
-member? {A} (x : A) : UnbalancedSet A -> Bool
-  | (unbalancedSet o@(mkOrd cmp) t) :=
-    let
-      go : BinaryTree A -> Bool
-        | leaf := false
-        | (node l y r) :=
-          case cmp x y of
-            | Ord.LT := go l
-            | Ord.GT := go r
-            | Ord.EQ := true;
-    in go t;
-
-insert {A} (x : A) : UnbalancedSet A -> UnbalancedSet A
-  | (unbalancedSet o@(mkOrd cmp) t) :=
-    let
-      go : BinaryTree A -> BinaryTree A
-        | leaf := node leaf x leaf
-        | n@(node l y r) :=
-          case cmp x y of
-            | Ord.LT := node (go l) y r
-            | Ord.EQ := n
-            | Ord.GT := node l y (go r);
-    in unbalancedSet o (go t);
-
-length {A} : UnbalancedSet A -> Nat
-  | (unbalancedSet _ t) := Tree.length t;
-
-to-list {A} : UnbalancedSet A -> List A
-  | (unbalancedSet _ t) := Tree.to-list t;
+type UnbalancedSet (A : Type) :=
+  mkUnbalancedSet {
+    order : Ord A;
+    tree : BinaryTree A
+  };
+
+empty {A} {{order : Ord A}} : UnbalancedSet A := mkUnbalancedSet order leaf;
+
+isMember {A} (elem : A) (set : UnbalancedSet A) : Bool :=
+  case set of
+    mkUnbalancedSet@{tree} :=
+      let
+        go : BinaryTree A -> Bool
+          | leaf := false
+          | node@{element; left; right} :=
+            case Ord.cmp elem element of
+              | Ord.LessThan := go left
+              | Ord.GreaterThan := go right
+              | Ord.Equal := true;
+      in go tree;
+
+insert {A} (elem : A) (set : UnbalancedSet A) : UnbalancedSet A :=
+  case set of
+    mkUnbalancedSet@{order; tree} :=
+      let
+        go : BinaryTree A -> BinaryTree A
+          | leaf := node leaf elem leaf
+          | tree@(node l y r) :=
+            case Ord.cmp elem y of
+              | Ord.LessThan := node (go l) y r
+              | Ord.Equal := tree
+              | Ord.GreaterThan := node l y (go r);
+      in mkUnbalancedSet order (go tree);
+
+length {A} (set : UnbalancedSet A) : Nat := Tree.length (UnbalancedSet.tree set);
+
+toList {A} (set : UnbalancedSet A) : List A := Tree.toList (UnbalancedSet.tree set);
 
 instance
-set-ordering {A} {{Ord A}} : Ord (UnbalancedSet A) :=
-  mkOrd λ {s1 s2 := Ord.cmp (to-list s1) (to-list s2)};
+unbalancedSetOrdI {A} {{Ord A}} : Ord (UnbalancedSet A) :=
+  mkOrd@{
+    cmp (s1 s2 : UnbalancedSet A) : Ordering := Ord.cmp (toList s1) (toList s2)
+  };
diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix
index e3952ffe..5602f05a 100644
--- a/Stdlib/Data/Unit.juvix
+++ b/Stdlib/Data/Unit.juvix
@@ -3,6 +3,7 @@ module Stdlib.Data.Unit;
 
 import Stdlib.Data.Unit.Base open public;
 import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.String.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
@@ -10,20 +11,31 @@ import Stdlib.Trait.Show open;
 import Stdlib.Trait.Foldable open;
 
 instance
-eqUnitI : Eq Unit := mkEq λ {unit unit := true};
+eqUnitI : Eq Unit :=
+  mkEq@{
+    eq (_ _ : Unit) : Bool := true
+  };
 
 instance
-ordUnitI : Ord Unit := mkOrd λ {unit unit := EQ};
+ordUnitI : Ord Unit :=
+  mkOrd@{
+    cmp (_ _ : Unit) : Ordering := Equal
+  };
 
 instance
-showUnitI : Show Unit := mkShow λ {unit := "unit"};
+showUnitI : Show Unit :=
+  mkShow@{
+    show (_ : Unit) : String := "unit"
+  };
 
 {-# specialize: true, inline: case #-}
 instance
 foldableUnitI : Foldable Unit Unit :=
   mkFoldable@{
     {-# inline: true #-}
-    rfor {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit;
+    rfor {Acc : Type} (fun : Acc -> Unit -> Acc) (initialValue : Acc) (_ : Unit) : Acc :=
+      fun initialValue unit;
     {-# inline: true #-}
-    for {B : Type} (f : B -> Unit -> B) (ini : B) (_ : Unit) : B := f ini unit
+    for {Acc : Type} (fun : Acc -> Unit -> Acc) (initialValue : Acc) (_ : Unit) : Acc :=
+      fun initialValue unit
   };
diff --git a/Stdlib/Debug/Fail.juvix b/Stdlib/Debug/Fail.juvix
index 9eaf4d60..45a106e6 100644
--- a/Stdlib/Debug/Fail.juvix
+++ b/Stdlib/Debug/Fail.juvix
@@ -2,6 +2,6 @@ module Stdlib.Debug.Fail;
 
 import Stdlib.Data.String.Base open;
 
---- Primitive that exits the program with an error message.
+--- Exit the program with an error message.
 builtin fail
-axiom failwith : {A : Type} → String → A;
+axiom failwith : {A : Type} -> (message : String) -> A;
diff --git a/Stdlib/Debug/Trace.juvix b/Stdlib/Debug/Trace.juvix
index 5495df18..b26d0c01 100644
--- a/Stdlib/Debug/Trace.juvix
+++ b/Stdlib/Debug/Trace.juvix
@@ -2,4 +2,4 @@ module Stdlib.Debug.Trace;
 
 --- Primitive that prints the given element and returns it.
 builtin trace
-axiom trace : {A : Type} → A → A;
+axiom trace : {A : Type} -> A -> A;
diff --git a/Stdlib/Extra/Gcd.juvix b/Stdlib/Extra/Gcd.juvix
index 5c7455d0..5a7d778b 100644
--- a/Stdlib/Extra/Gcd.juvix
+++ b/Stdlib/Extra/Gcd.juvix
@@ -6,11 +6,16 @@ import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Data.Bool open;
 
---- Computes the greatest common divisor.
+--- Computes the greatest common divisor of `a` and `b`.
 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.
     terminating
-    gcd' (a b : A) : A := ite (a == 0) b (gcd' (mod b a) a);
-  in ite (a > b) (gcd' b a) (gcd' a b);
+    gcd' (a b : A) : A :=
+      if
+        | a == 0 := b
+        | else := gcd' (mod b a) a;
+  in if
+    | a > b := gcd' b a
+    | else := gcd' a b;
diff --git a/Stdlib/Function.juvix b/Stdlib/Function.juvix
index c1b9e53e..2cdf6874 100644
--- a/Stdlib/Function.juvix
+++ b/Stdlib/Function.juvix
@@ -6,51 +6,52 @@ import Stdlib.Data.Pair.Base open;
 
 syntax operator << composition;
 
---- Function composition, passing results from the second function to the first.
+--- Function composition, passing results from the second function `g` to the first function `f`.
 {-# inline: 2 #-}
-<< {A B C} (f : B → C) (g : A → B) (x : A) : C := f (g x);
+<< {A B C} (f : B -> C) (g : A -> B) (x : A) : C := f (g x);
 
 syntax operator >> lcomposition;
 
---- Function composition, passing results from the first function to the second.
+--- Function composition, passing results from the first function `f` to the second function `g`.
 {-# inline: 2 #-}
->> {A B C} (f : A → B) (g : B → C) (x : A) : C := g (f x);
+>> {A B C} (f : A -> B) (g : B -> C) (x : A) : C := g (f x);
 
---- Always returns the first argument.
+--- Always returns the first argument `a`.
 {-# inline: 1 #-}
 const {A B} (a : A) (_ : B) : A := a;
 
 --- The identity function.
 id {A} (a : A) : A := a;
 
---- Swaps the order of the arguments of the given function.
+--- Swaps the order of the arguments of the given function `f`.
 {-# inline: 1 #-}
-flip {A B C} (f : A → B → C) (b : B) (a : A) : C := 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 B} (f : A → B) (x : A) : B := f x;
+<| {A B} (f : A -> B) (x : A) : B := f x;
 
 syntax operator |> lapp;
 
 --- Application operator with left associativity. Usually used as a syntactical
 --- facility.
-|> {A B} (x : A) (f : A → B) : B := f x;
+|> {A B} (x : A) (f : A -> B) : B := f x;
 
 --- Applies a function n times.
-iterate {A} : Nat -> (A -> A) -> A -> A
+iterate {A} : (n : Nat) -> (fun : A -> A) -> (elem : A) -> A
   | zero _ a := a
   | (suc n) f a := iterate n f (f a);
 
 syntax operator on lapp;
 
+--- `(f on g) a b` is equivalent to `f (g a) (g b)`.
 {-# 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;
 
 builtin seq
->-> : {A B : Type} → A → B → B
+>-> : {A B : Type} -> A -> B -> B
   | x y := y;
diff --git a/Stdlib/System/IO/Base.juvix b/Stdlib/System/IO/Base.juvix
index 67722245..1277b331 100644
--- a/Stdlib/System/IO/Base.juvix
+++ b/Stdlib/System/IO/Base.juvix
@@ -7,4 +7,4 @@ axiom IO : Type;
 
 syntax operator >>> seq;
 builtin IO-sequence
-axiom >>> : IO → IO → IO;
+axiom >>> : IO -> IO -> IO;
diff --git a/Stdlib/System/IO/Bool.juvix b/Stdlib/System/IO/Bool.juvix
index 23e53233..8fdecece 100644
--- a/Stdlib/System/IO/Bool.juvix
+++ b/Stdlib/System/IO/Bool.juvix
@@ -5,6 +5,6 @@ import Stdlib.Data.Bool open;
 import Stdlib.System.IO.String open;
 
 builtin bool-print
-axiom printBool : Bool → IO;
+axiom printBool : Bool -> IO;
 
 printBoolLn (b : Bool) : IO := printBool b >>> printString "\n";
diff --git a/Stdlib/System/IO/Int.juvix b/Stdlib/System/IO/Int.juvix
index abe531e8..66f9214a 100644
--- a/Stdlib/System/IO/Int.juvix
+++ b/Stdlib/System/IO/Int.juvix
@@ -5,6 +5,6 @@ import Stdlib.Data.Int open using {Int};
 import Stdlib.System.IO.String open;
 
 builtin int-print
-axiom printInt : Int → IO;
+axiom printInt : Int -> IO;
 
 printIntLn (i : Int) : IO := printInt i >>> printString "\n";
diff --git a/Stdlib/System/IO/Nat.juvix b/Stdlib/System/IO/Nat.juvix
index 8f787ae6..d21359b8 100644
--- a/Stdlib/System/IO/Nat.juvix
+++ b/Stdlib/System/IO/Nat.juvix
@@ -5,6 +5,6 @@ import Stdlib.Data.Nat open;
 import Stdlib.System.IO.String open;
 
 builtin nat-print
-axiom printNat : Nat → IO;
+axiom printNat : Nat -> IO;
 
 printNatLn (n : Nat) : IO := printNat n >>> printString "\n";
diff --git a/Stdlib/System/IO/String.juvix b/Stdlib/System/IO/String.juvix
index e79c8668..4685d322 100644
--- a/Stdlib/System/IO/String.juvix
+++ b/Stdlib/System/IO/String.juvix
@@ -4,9 +4,9 @@ import Stdlib.System.IO.Base open;
 import Stdlib.Data.String open;
 
 builtin string-print
-axiom printString : String → IO;
+axiom printString : String -> IO;
 
 builtin IO-readline
-axiom readLn : (String → IO) → IO;
+axiom readLn : (String -> IO) -> IO;
 
 printStringLn (s : String) : IO := printString s >>> printString "\n";
diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix
index d556da7c..d6e6c596 100644
--- a/Stdlib/Trait/Applicative.juvix
+++ b/Stdlib/Trait/Applicative.juvix
@@ -11,22 +11,22 @@ import Stdlib.Trait.Foldable.Polymorphic open;
 import Stdlib.Data.Unit.Base open;
 
 trait
-type Applicative (f : Type -> Type) :=
+type Applicative (F : Type -> Type) :=
   mkApplicative {
-    {{functor}} : Functor f;
-    pure : {A : Type} -> A -> f A;
-    ap : {A B : Type} -> f (A -> B) -> f A -> f B
+    {{functor}} : Functor F;
+    pure : {A : Type} -> A -> F A;
+    ap : {A B : Type} -> F (A -> B) -> F A -> F B
   };
 
 open Applicative public;
 
 --- Sequences computations.
 --- Note that this function will be renamed to >>> once IO becomses a polymorphic type and can be given an Applicative instance.
-applicativeSeq {f : Type -> Type} {{Applicative f}} {A B : Type} (fa : f A) (fb : f B) : f B :=
+applicativeSeq {F : Type -> Type} {{Applicative F}} {A B : Type} (fa : F A) (fb : F B) : F B :=
   ap (map λ {_ b := b} fa) fb;
 
 --- lifts a binary function to ;Applicative;
-liftA2 {f : Type -> Type} {{Applicative f}} {A B C} (fun : A -> B -> C) : f A -> f B -> f C :=
+liftA2 {F : Type -> Type} {{Applicative F}} {A B C} (fun : A -> B -> C) : F A -> F B -> F C :=
   map fun >> ap;
 
 syntax iterator mapA_ {init := 0; range := 1};
@@ -40,10 +40,10 @@ mapA_
   (l : t A)
   : f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc};
 
-replicateA {f : Type -> Type} {A} {{Applicative f}} : Nat -> f A -> f (List A)
+replicateA {F : Type -> Type} {A} {{Applicative F}} : Nat -> F A -> F (List A)
   | zero _ := pure []
   | (suc n) x := liftA2 (::) x (replicateA n x);
 
-when {f : Type -> Type} {{Applicative f}} : Bool -> f Unit -> f Unit
+when {F : Type -> Type} {{Applicative F}} : Bool -> F Unit -> F Unit
   | false _ := pure unit
   | true a := a;
diff --git a/Stdlib/Trait/Eq.juvix b/Stdlib/Trait/Eq.juvix
index 9ccb3c4d..787809e1 100644
--- a/Stdlib/Trait/Eq.juvix
+++ b/Stdlib/Trait/Eq.juvix
@@ -13,6 +13,6 @@ syntax operator /= comparison;
 {-# inline: always, isabelle-operator: {name: "=", prec: 50, assoc: none} #-}
 == {A} {{Eq A}} : A -> A -> Bool := Eq.eq;
 
---- Tests for inequality.
+--- Test for inequality.
 {-# inline: always, isabelle-operator: {name: "\\<noteq>", prec: 50, assoc: none} #-}
 /= {A} {{Eq A}} (x y : A) : Bool := not (x == y);
diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
index 319e62cc..e546414f 100644
--- a/Stdlib/Trait/Foldable/Monomorphic.juvix
+++ b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -6,13 +6,13 @@ import Stdlib.Trait.Foldable.Polymorphic as Poly;
 --- A trait for combining elements into a single result, processing one element at a time.
 {-# specialize: true #-}
 trait
-type Foldable (container elem : Type) :=
+type Foldable (Container Elem : Type) :=
   mkFoldable {
     syntax iterator for {init := 1; range := 1};
-    for : {B : Type} -> (B -> elem -> B) -> B -> container -> B;
+    for : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B;
 
     syntax iterator rfor {init := 1; range := 1};
-    rfor : {B : Type} -> (B -> elem -> B) -> B → container → B
+    rfor : {B : Type} -> (B -> Elem -> B) -> B -> Container -> B
   };
 
 open Foldable public;
@@ -21,7 +21,7 @@ open Foldable public;
 --- All polymorphic types that are an instance of ;Poly.Foldable; should use this function to create their monomorphic ;Foldable; instance.
 {-# inline: case #-}
 fromPolymorphicFoldable
-  {f : Type -> Type} {{foldable : Poly.Foldable f}} {elem} : Foldable (f elem) elem :=
+  {F : Type -> Type} {{foldable : Poly.Foldable F}} {Elem} : Foldable (F Elem) Elem :=
   mkFoldable@{
     for := Poly.for;
     rfor := Poly.rfor
@@ -29,19 +29,21 @@ fromPolymorphicFoldable
 
 {-# inline: true #-}
 foldl
-  {container elem}
-  {{Foldable container elem}}
-  {B : Type}
-  (g : B -> elem -> B)
-  (ini : B)
-  (ls : container)
-  : B := for (acc := ini) (x in ls) {g acc x};
+  {Container Elem}
+  {{Foldable Container Elem}}
+  {Acc : Type}
+  (fun : Acc -> Elem -> Acc)
+  (initialValue : Acc)
+  (container : Container)
+  : Acc := for (acc := initialValue) (x in container) {fun acc x};
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
 {-# inline: 2 #-}
 foldr
-  {container elem : Type}
-  {{Foldable container elem}}
-  {B : Type}
-  (g : elem -> B -> B)
-  : B -> container -> B := foldl (flip g);
+  {Container Elem : Type}
+  {{Foldable Container Elem}}
+  {Acc : Type}
+  (fun : Elem -> Acc -> Acc)
+  (initialValue : Acc)
+  (container : Container)
+  : Acc := foldl (flip fun) initialValue container;
diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix
index 624cb6cb..45d813e1 100644
--- a/Stdlib/Trait/Foldable/Polymorphic.juvix
+++ b/Stdlib/Trait/Foldable/Polymorphic.juvix
@@ -4,23 +4,35 @@ import Stdlib.Function open;
 
 --- A trait for combining elements into a single result, processing one element at a time.
 trait
-type Foldable (f : Type -> Type) :=
+type Foldable (F : Type -> Type) :=
   mkFoldable {
     syntax iterator for {init := 1; range := 1};
-    for : {A B : Type} -> (B -> A -> B) -> B -> f A -> B;
+    for : {A B : Type} -> (B -> A -> B) -> B -> F A -> B;
 
     syntax iterator rfor {init := 1; range := 1};
-    rfor : {A B : Type} -> (B → A → B) -> B → f A → B
+    rfor : {A B : Type} -> (B -> A -> B) -> B -> F A -> B
   };
 
 open Foldable public;
 
 --- Combine the elements of the type using the provided function starting with the element in the left-most position.
 {-# inline: true #-}
-foldl {f : Type -> Type} {{Foldable f}} {A B : Type} (g : B -> A -> B) (ini : B) (ls : f A) : B :=
-  for (acc := ini) (x in ls) {g acc x};
+foldl
+  {F : Type -> Type}
+  {{Foldable F}}
+  {Elem Acc : Type}
+  (fun : Acc -> Elem -> Acc)
+  (initialValue : Acc)
+  (container : F Elem)
+  : Acc := for (acc := initialValue) (x in container) {fun acc x};
 
 --- Combine the elements of the type using the provided function starting with the element in the right-most position.
 {-# inline: true #-}
-foldr {f : Type -> Type} {{Foldable f}} {A B : Type} (g : A -> B -> B) (ini : B) (ls : f A) : B :=
-  rfor (acc := ini) (x in ls) {g x acc};
+foldr
+  {F : Type -> Type}
+  {{Foldable F}}
+  {Elem Acc : Type}
+  (fun : Elem -> Acc -> Acc)
+  (initialValue : Acc)
+  (container : F Elem)
+  : Acc := rfor (acc := initialValue) (x in container) {fun x acc};
diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix
index c5c188e2..8a4343ad 100644
--- a/Stdlib/Trait/Functor/Monomorphic.juvix
+++ b/Stdlib/Trait/Functor/Monomorphic.juvix
@@ -6,26 +6,35 @@ import Stdlib.Trait.Functor.Polymorphic as Poly;
 
 {-# specialize: true #-}
 trait
-type Functor (container elem : Type) :=
+type Functor (Container Elem : Type) :=
   mkFunctor {
     syntax iterator map {init := 0; range := 1};
     {-# specialize: [1] #-}
-    map : (elem -> elem) -> container -> container
+    map : (Elem -> Elem) -> Container -> Container
   };
 
 open Functor public;
 
 {-# inline: case #-}
-fromPolymorphicFunctor {f : Type -> Type} {{Poly.Functor f}} {elem} : Functor (f elem) elem :=
+fromPolymorphicFunctor {F : Type -> Type} {{Poly.Functor F}} {Elem} : Functor (F Elem) Elem :=
   mkFunctor@{
     map := Poly.map
   };
 
 syntax operator <$> lapp;
 {-# inline: true #-}
-<$> {container elem} {{Functor container elem}} : (elem -> elem) -> container -> container := map;
+<$>
+  {Container Elem}
+  {{Functor Container Elem}}
+  (fun : Elem -> Elem)
+  (container : Container)
+  : Container := map fun container;
 
 syntax operator $> lapp;
 {-# inline: true #-}
-$> {container elem : Type} {{Functor container elem}} (fa : container) (b : elem) : container :=
-  λ {_ := b} <$> fa;
+$>
+  {Container Elem : Type}
+  {{Functor Container Elem}}
+  (container : Container)
+  (element : Elem)
+  : Container := \ {_ := element} <$> container;
diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix
index 37b12c02..6fd60520 100644
--- a/Stdlib/Trait/Functor/Polymorphic.juvix
+++ b/Stdlib/Trait/Functor/Polymorphic.juvix
@@ -5,22 +5,22 @@ import Stdlib.Data.Unit open;
 
 {-# specialize: true #-}
 trait
-type Functor (f : Type -> Type) :=
+type Functor (F : Type -> Type) :=
   mkFunctor {
     syntax iterator map {init := 0; range := 1};
     {-# specialize: [1] #-}
-    map : {A B : Type} -> (A -> B) -> f A -> f B
+    map : {A B : Type} -> (A -> B) -> F A -> F B
   };
 
 open Functor public;
 
 syntax operator <$> lapp;
 {-# inline: true #-}
-<$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f B := map;
+<$> {F : Type -> Type} {{Functor F}} {A B} (fun : A -> B) (fa : F A) : F B := map fun fa;
 
 syntax operator $> lapp;
 {-# inline: true #-}
-$> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B := λ {_ := b} <$> fa;
+$> {F : Type → Type} {A B : Type} {{Functor F}} (fa : F A) (b : B) : F B := λ {_ := b} <$> fa;
 
 {-# inline: true #-}
-void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := fa $> unit;
+void {F : Type → Type} {A : Type} {{Functor F}} (fa : F A) : F Unit := fa $> unit;
diff --git a/Stdlib/Trait/Monad.juvix b/Stdlib/Trait/Monad.juvix
index 8197b4b4..e59ee45d 100644
--- a/Stdlib/Trait/Monad.juvix
+++ b/Stdlib/Trait/Monad.juvix
@@ -4,17 +4,17 @@ import Stdlib.Data.Fixity open;
 import Stdlib.Trait.Applicative open;
 
 trait
-type Monad (m : Type -> Type) :=
+type Monad (M : Type -> Type) :=
   mkMonad {
-    {{applicative}} : Applicative m;
+    {{applicative}} : Applicative M;
     builtin monad-bind
-    bind : {A B : Type} -> m A -> (A -> m B) -> m B
+    bind : {A B : Type} -> M A -> (A -> M B) -> M B
   };
 
 open Monad public;
 
 syntax operator >>= seq;
->>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g;
+>>= {A B} {F : Type -> Type} {{Monad F}} (x : F A) (g : A -> F B) : F B := bind x g;
 
 syntax operator >=> seq;
->=> {A B C} {f : Type -> Type} {{Monad f}} (h : A -> f B) (g : B -> f C) (a : A) : f C := h a >>= g;
+>=> {A B C} {F : Type -> Type} {{Monad F}} (h : A -> F B) (g : B -> F C) (a : A) : F C := h a >>= g;
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index 8573c4ba..9d3e2a24 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -5,29 +5,33 @@ import Stdlib.Data.Bool.Base open;
 import Stdlib.Trait.Eq open;
 
 type Ordering :=
-  | LT : Ordering
-  | EQ : Ordering
-  | GT : Ordering;
+  | LessThan
+  | Equal
+  | GreaterThan;
 
-isLT : Ordering → Bool
-  | LT := true
-  | _ := false;
+isLessThan (ordering : Ordering) : Bool :=
+  case ordering of
+    | LessThan := true
+    | _ := false;
 
-isEQ : Ordering → Bool
-  | EQ := true
-  | _ := false;
+isEqual (ordering : Ordering) : Bool :=
+  case ordering of
+    | Equal := true
+    | _ := false;
 
-isGT : Ordering → Bool
-  | GT := true
-  | _ := false;
+isGreaterThan (ordering : Ordering) : Bool :=
+  case ordering of
+    | GreaterThan := true
+    | _ := false;
 
 instance
 orderingEqI : Eq Ordering :=
   mkEq@{
-    eq (x : Ordering) : Ordering -> Bool
-      | LT := isLT x
-      | EQ := isEQ x
-      | GT := isGT x
+    eq (ordering1 ordering2 : Ordering) : Bool :=
+      case ordering2 of
+        | LessThan := isLessThan ordering1
+        | Equal := isEqual ordering1
+        | GreaterThan := isGreaterThan ordering1
   };
 
 --- A trait for defining a total order
@@ -40,9 +44,9 @@ syntax operator <= comparison;
 {-# inline: always, isabelle-operator: {name: "\\<le>", prec: 50, assoc: none} #-}
 <= {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
-    | EQ := true
-    | LT := true
-    | GT := false;
+    | Equal := true
+    | LessThan := true
+    | GreaterThan := false;
 
 syntax operator < comparison;
 
@@ -50,9 +54,9 @@ syntax operator < comparison;
 {-# inline: always, isabelle-operator: {name: "<", prec: 50, assoc: none} #-}
 < {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
-    | EQ := false
-    | LT := true
-    | GT := false;
+    | Equal := false
+    | LessThan := true
+    | GreaterThan := false;
 
 syntax operator > comparison;
 
@@ -68,8 +72,14 @@ syntax operator >= comparison;
 
 --- Returns the smaller element.
 {-# inline: always #-}
-min {A} {{Ord A}} (x y : A) : A := ite (x < y) x y;
+min {A} {{Ord A}} (x y : A) : A :=
+  if
+    | x < y := x
+    | else := y;
 
 --- Returns the larger element.
 {-# inline: always #-}
-max {A} {{Ord A}} (x y : A) : A := ite (x > y) x y;
+max {A} {{Ord A}} (x y : A) : A :=
+  if
+    | x > y := x
+    | else := y;
diff --git a/Stdlib/Trait/Ord/Eq.juvix b/Stdlib/Trait/Ord/Eq.juvix
index c4e90751..9e690469 100644
--- a/Stdlib/Trait/Ord/Eq.juvix
+++ b/Stdlib/Trait/Ord/Eq.juvix
@@ -12,7 +12,7 @@ syntax operator == comparison;
 {-# isabelle-operator: {name: "=", prec: 50, assoc: none} #-}
 == {A} {{Ord A}} (x y : A) : Bool :=
   case Ord.cmp x y of
-    | EQ := true
+    | Equal := true
     | _ := false;
 
 syntax operator /= comparison;
diff --git a/test/Package.juvix b/test/Package.juvix
index 8b63758a..ca94b3e0 100644
--- a/test/Package.juvix
+++ b/test/Package.juvix
@@ -7,7 +7,7 @@ package : Package :=
     name := "stdlib-test";
     dependencies :=
       [ path "../"
-      ; github "anoma" "juvix-quickcheck" "b398d3cd58f0a7fb9be24d57fc5b3d82f31de555"
-      ; github "anoma" "juvix-test" "3103c41e055eb9018a851fd3688cd608cad8f55d"
+      ; github "anoma" "juvix-quickcheck" "4242b864714f98947753544ea1b2cb435f6473d3"
+      ; github "anoma" "juvix-test" "85811914324b082549cb1f500323884442fc793c"
       ]
   };
diff --git a/test/Test.juvix b/test/Test.juvix
index 49f8281c..f52e4311 100644
--- a/test/Test.juvix
+++ b/test/Test.juvix
@@ -17,118 +17,102 @@ import Test.Map open using {suite as mapSuite};
 import Test.Queue open using {suite as queueSuite};
 import Test.UnbalancedSet open using {suite as unbalancedSetSuite};
 
-prop-reverseDoesNotChangeLength : List Int -> Bool
-  | xs := length (reverse xs) == 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 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;
--- Make sure the list has length at least n
-
-prop-mergeSumLengths : List Int -> List Int -> Bool
-  | xs ys := length xs + length ys == length (merge xs ys);
-
-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));
-
-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 == ofNat 2;
-
-prop-gcd-bad : Int -> Int -> Bool
-  | a b := gcd a b > ofNat 1;
-
-prop-equal-compare-to-eq : Nat -> Bool
-  | a := Ord.isEQ (Ord.cmp 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 == length xs && eqListInt sorted (sort sorted) && isSorted sorted;
-
-prop-zip : List Int -> List Int -> Bool
-  | xs ys :=
-    let
-      zs : List (Pair Int Int) := zip xs ys;
-      expectedLen : Nat := min (length xs) (length ys);
-    in length zs == 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 := min (length xs) (length ys);
-    in length zs == 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 <= length xs && eqListInt (drop n (drop n xs)) (drop (2 * n) xs);
+propReverseDoesNotChangeLength (xs : List Int) : Bool := length (reverse xs) == length xs;
+
+propReverseReverseIsIdentity (xs : List Int) : Bool := eqListInt xs (reverse (reverse xs));
+
+propTailLengthOneLess (xs : List Int) : Bool :=
+  null xs || ofNat (length (tail xs)) == intSubNat (length xs) 1;
+
+propSplitAtRecombine (n : Nat) (xs : List Int) : Bool :=
+  case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs);
+
+propSplitAtLength (n : Nat) (xs : List Int) : Bool :=
+  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 (TODO: make sure where?)
+
+propMergeSumLengths (xs ys : List Int) : Bool := length xs + length ys == length (merge xs ys);
+
+propPartition (xs : List Int) (predicate : Int -> Bool) : Bool :=
+  case partition predicate xs of
+    lhs, rhs :=
+      all predicate lhs && not (any predicate rhs) && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
+
+propDistributive (a b : Int) (f : Int -> Int) : Bool := f (a + b) == f a + f b;
+
+propAddSub (a b : Int) : Bool := a == a + b - b;
+
+propAddSubBad (a b : Int) : Bool := a == ofNat 2;
+
+propGcdBad (a b : Int) : Bool := gcd a b > ofNat 1;
+
+propEqualCompareToEq (a : Nat) : Bool := Ord.isEqual (Ord.cmp a a);
+
+propSort (sort : List Int -> List Int) (xs : List Int) : Bool :=
+  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 == length xs && eqListInt sorted (sort sorted) && isSorted sorted;
+
+propZip (xs ys : List Int) : Bool :=
+  let
+    zs : List (Pair Int Int) := zip xs ys;
+    expectedLen : Nat := min (length xs) (length ys);
+  in length zs == expectedLen
+    && eqListInt (take expectedLen xs) (map fst zs)
+    && eqListInt (take expectedLen ys) (map snd zs);
+
+propZipWith (f : Int -> Int -> Int) (xs ys : List Int) : Bool :=
+  let
+    zs : List Int := zipWith f xs ys;
+    zsFlip : List Int := zipWith (flip f) ys xs;
+    expectedLen : Nat := min (length xs) (length ys);
+  in length zs == expectedLen
+    && eqListInt zs zsFlip
+    && eqListInt (map λ {x := f x x} xs) (zipWith f xs xs);
+
+propSnoc (xs : List Int) (x : Int) : Bool :=
+  let
+    snoc-x : List Int := snoc xs x;
+  in eqListInt snoc-x (reverse (x :: reverse xs));
+
+propDrop (n : Nat) (xs : List Int) : Bool :=
+  let
+    drop-n : List Int := drop 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
-  | xs := Eq.eq xs (transpose (transpose xs));
+propTransposeMatrixId (xs : List (List Int)) : Bool := Eq.eq xs (transpose (transpose xs));
 
 -- Assumption: The input list represents a rectangular matrix
-prop-transposeMatrixDimensions : List (List Int) -> Bool
-  | xs :=
-    let
-      txs : List (List Int) := transpose xs;
-      checkTxsRowXsCol : Bool :=
-        case xs of
-          | x :: _ := length txs == length x
-          | _ := null txs;
-      checkXsRowTxsCol : Bool :=
-        case txs of
-          | tx :: _ := length xs == length tx
-          | _ := null xs;
-    in checkTxsRowXsCol && checkXsRowTxsCol;
-
-prop-foundElementSatisfiesPredicate (p : Int -> Bool) (xs : List Int) : Bool :=
+propTransposeMatrixDimensions (xs : List (List Int)) : Bool :=
+  let
+    txs : List (List Int) := transpose xs;
+    checkTxsRowXsCol : Bool :=
+      case xs of
+        | x :: _ := length txs == length x
+        | _ := null txs;
+    checkXsRowTxsCol : Bool :=
+      case txs of
+        | tx :: _ := length xs == length tx
+        | _ := null xs;
+  in checkTxsRowXsCol && checkXsRowTxsCol;
+
+propFoundElementSatisfiesPredicate (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 :=
+propNonExistenceImpliesPredicateFalseForAll (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 :=
+propFindConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool :=
   let
     ys×zs := splitAt n xs;
     ys := fst ys×zs;
@@ -136,14 +120,14 @@ prop-findConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Boo
   in case find p xs of
        | just x :=
          if
-           | elem (==) x ys := find p ys == just x
-           | elem (==) x zs := find p zs == just x
+           | isMember x ys := find p ys == just x
+           | isMember x zs := find p zs == just x
            | else := false
        | nothing := true;
 
-prop-findWithEmptyList (p : Int -> Bool) : Bool := find p [] == nothing;
+propFindWithEmptyList (p : Int -> Bool) : Bool := find p [] == nothing;
 
-prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool :=
+propFindWithAlwaysTrueIsJust (xs : List Int) : Bool :=
   if
     | null xs := true
     | else :=
@@ -151,140 +135,148 @@ prop-findWithAlwaysTrueIsJust (xs : List Int) : Bool :=
         | just _ := true
         | nothing := false;
 
-prop-findWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing;
+propFindWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing;
 
-prop-resultErrorApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
+propResultErrorApplication (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 :=
+propResultOkApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
   handleResult f g (ok x) == g x;
 
-prop-resultIsError : Result Int Bool -> Bool
-  | x@(error _) := isError x
-  | x@(ok _) := not (isError x);
+propResultIsError (result : Result Int Bool) : Bool :=
+  case result of
+    | error _ := isError result
+    | ok _ := not (isError result);
 
-prop-resultIsOk : Result Int Bool -> Bool
-  | x@(error _) := not (isOk x)
-  | x@(ok _) := isOk x;
+propResultIsOk (result : Result Int Bool) : Bool :=
+  case result of
+    | error _ := not (isOk result)
+    | ok _ := isOk result;
 
-prop-resultFromErrorDefault (defaultError : Int) : Result Int Bool -> Bool
-  | e@(error x) := fromError defaultError e == x
-  | e@(ok _) := fromError defaultError e == defaultError;
+propResultFromErrorDefault (defaultError : Int) (result : Result Int Bool) : Bool :=
+  case result of
+    | error x := fromError defaultError result == x
+    | ok _ := fromError defaultError result == defaultError;
 
-prop-resultFromOkDefault (defaultOk : Bool) : Result Int Bool -> Bool
-  | e@(error _) := fromOk defaultOk e == defaultOk
-  | e@(ok x) := fromOk defaultOk e == x;
+propResultFromOkDefault (defaultOk : Bool) (result : Result Int Bool) : Bool :=
+  case result of
+    | error _ := fromOk defaultOk result == defaultOk
+    | ok x := fromOk defaultOk result == x;
 
-prop-resultToMaybe : Result Int Bool -> Bool
-  | e@(error _) := resultToMaybe e == nothing
-  | e@(ok x) := resultToMaybe e == just x;
+propResultToMaybe (result : Result Int Bool) : Bool :=
+  case result of
+    | error _ := resultToMaybe result == nothing
+    | ok x := resultToMaybe result == just x;
 
-prop-maybeToResult (def : Int) : Maybe Bool -> Bool
-  | m@(just x) := maybeToResult def m == ok x
-  | m@nothing := maybeToResult def m == error def;
+propMaybeToResult (def : Int) (maybe : Maybe Bool) : Bool :=
+  case maybe of
+    | just x := maybeToResult def maybe == ok x
+    | nothing := maybeToResult def maybe == error def;
 
-prop-resultMapError (f : Int -> Int) : Result Int Int -> Bool
-  | e@(error x) := mapError f e == error (f x)
-  | e@(ok _) := mapError f e == e;
+propResultMapError (f : Int -> Int) (result : Result Int Int) : Bool :=
+  case result of
+    | error x := mapError f result == error (f x)
+    | ok _ := mapError f result == result;
 
-prop-resultMapOk (f : Int -> Int) : Result Int Int -> Bool
-  | e@(error _) := mapOk f e == e
-  | e@(ok x) := mapOk f e == ok (f x);
+propResultMapOk (f : Int -> Int) (result : Result Int Int) : Bool :=
+  case result of
+    | error _ := mapOk f result == result
+    | ok x := mapOk f result == ok (f x);
 
-sortTest : String -> (List Int -> List Int) -> QC.Test
-  | sortName sort := QC.mkTest ("sort properties: " ++str sortName) (prop-sort sort);
+sortTest (sortName : String) (sort : List Int -> List Int) : QC.Test :=
+  QC.mkTest ("sort properties: " ++str sortName) (propSort sort);
 
-dropTest : QC.Test := QC.mkTest "drop properties" prop-drop;
+dropTest : QC.Test := QC.mkTest "drop properties" propDrop;
 
-snocTest : QC.Test := QC.mkTest "snoc properties" prop-snoc;
+snocTest : QC.Test := QC.mkTest "snoc properties" propSnoc;
 
-zipTest : QC.Test := QC.mkTest "zip properties" prop-zip;
+zipTest : QC.Test := QC.mkTest "zip properties" propZip;
 
-zipWithTest : QC.Test := QC.mkTest "zipWith properties" prop-zipWith;
+zipWithTest : QC.Test := QC.mkTest "zipWith properties" propZipWith;
 
-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" propEqualCompareToEq;
 
-gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" prop-gcd-bad;
+gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" propGcdBad;
 
 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" propPartition;
 
-testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" prop-distributive;
+testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" propDistributive;
 
-reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" prop-reverseDoesNotChangeLength;
+reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" propReverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
-  QC.mkTest "reverse of reverse is identity" prop-reverseReverseIsIdentity;
+  QC.mkTest "reverse of reverse is identity" propReverseReverseIsIdentity;
 
 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" propSplitAtRecombine;
 
 splitAtLengthTest : QC.Test :=
   QC.mkTest
     "splitAt: Check lengths of output if the input Nat is greater than the length of the input list"
-    prop-splitAtLength;
+    propSplitAtLength;
 
 mergeSumLengthsTest : QC.Test :=
   QC.mkTest
     "merge: sum of the lengths of input lists is equal to the length of output list"
-    prop-mergeSumLengths;
+    propMergeSumLengths;
 
 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" propTailLengthOneLess;
 
 transposeMatrixIdTest : QC.Test :=
   QC.mkTest
     {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}}
     "transpose: recrangular matrix has property transpose . transpose = id"
-    prop-transposeMatrixId;
+    propTransposeMatrixId;
 
 transposeMatrixDimentionsTest : QC.Test :=
   QC.mkTest
     {{QC.testableFunction {{showListI}} {{QC.arbitraryMatrix}}}}
     "transpose: transpose swaps dimensions"
-    prop-transposeMatrixDimensions;
+    propTransposeMatrixDimensions;
 
 findFoundElementSatisfiesPredicate : QC.Test :=
-  QC.mkTest "find: found element satisfies predicate" prop-foundElementSatisfiesPredicate;
+  QC.mkTest "find: found element satisfies predicate" propFoundElementSatisfiesPredicate;
 
 findNonExistenceImpliesPredicateFalseForAll : QC.Test :=
   QC.mkTest
     "find: non existence implies predicate false for all"
-    prop-nonExistenceImpliesPredicateFalseForAll;
+    propNonExistenceImpliesPredicateFalseForAll;
 
 findConsistentWithSplitAt : QC.Test :=
-  QC.mkTest "find: consistent with splitAt" prop-findConsistentWithSplitAt;
+  QC.mkTest "find: consistent with splitAt" propFindConsistentWithSplitAt;
 
 findOnEmptyListIsNothing : QC.Test :=
-  QC.mkTest "find: called with empty list is nothing" prop-findWithEmptyList;
+  QC.mkTest "find: called with empty list is nothing" propFindWithEmptyList;
 
 findWithAlwaysTrueIsJust : QC.Test :=
-  QC.mkTest "find: always true predicate returns just" prop-findWithAlwaysTrueIsJust;
+  QC.mkTest "find: always true predicate returns just" propFindWithAlwaysTrueIsJust;
 
 findWithAlwaysFalseIsNothing : QC.Test :=
-  QC.mkTest "find: always false predicate returns nothing" prop-findWithAlwaysFalseIsNothing;
+  QC.mkTest "find: always false predicate returns nothing" propFindWithAlwaysFalseIsNothing;
 
 resultResultErrorApplication : QC.Test :=
-  QC.mkTest "result: result error application" prop-resultErrorApplication;
+  QC.mkTest "result: result error application" propResultErrorApplication;
 
 resultResultOkApplication : QC.Test :=
-  QC.mkTest "result: result ok application" prop-resultOkApplication;
+  QC.mkTest "result: result ok application" propResultOkApplication;
 
-resultIsError : QC.Test := QC.mkTest "result: isError detects error" prop-resultIsError;
+resultIsError : QC.Test := QC.mkTest "result: isError detects error" propResultIsError;
 
-resultIsOk : QC.Test := QC.mkTest "result: isOk detects ok" prop-resultIsOk;
+resultIsOk : QC.Test := QC.mkTest "result: isOk detects ok" propResultIsOk;
 
-resultFromError : QC.Test := QC.mkTest "result: fromError uses default" prop-resultFromErrorDefault;
+resultFromError : QC.Test := QC.mkTest "result: fromError uses default" propResultFromErrorDefault;
 
-resultFromOk : QC.Test := QC.mkTest "result: fromOk uses default" prop-resultFromOkDefault;
+resultFromOk : QC.Test := QC.mkTest "result: fromOk uses default" propResultFromOkDefault;
 
-resultResultToMaybe : QC.Test := QC.mkTest "result: resultToMaybe" prop-resultToMaybe;
+resultResultToMaybe : QC.Test := QC.mkTest "result: resultToMaybe" propResultToMaybe;
 
-resultMaybeToResult : QC.Test := QC.mkTest "result: maybeToResult" prop-maybeToResult;
+resultMaybeToResult : QC.Test := QC.mkTest "result: maybeToResult" propMaybeToResult;
 
-resultMapError : QC.Test := QC.mkTest "result: mapError" prop-resultMapError;
+resultMapError : QC.Test := QC.mkTest "result: mapError" propResultMapError;
 
-resultMapOk : QC.Test := QC.mkTest "result: mapOk" prop-resultMapOk;
+resultMapOk : QC.Test := QC.mkTest "result: mapOk" propResultMapOk;
 
 main : IO :=
   readLn
diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix
index 37c924b9..d70ab6a7 100644
--- a/test/Test/AVL.juvix
+++ b/test/Test/AVL.juvix
@@ -3,7 +3,7 @@ module Test.AVL;
 import Test.JuvixUnit open;
 import Stdlib.Prelude open;
 
-import Stdlib.Data.Set.AVL open;
+import Stdlib.Data.Set.AVL as AVL open;
 
 type Box := mkBox {b : Nat};
 
@@ -11,16 +11,17 @@ instance
 BoxOrdI : Ord Box := mkOrd (Ord.cmp on Box.b);
 
 --- Test for size and balance.
-mkTests {A} : TestDescr A -> List Test
-  | mkTestDescr@{testTitle; testLen; testSet} :=
-    let
-      mkTitle : String -> String
-        | m := testTitle ++str " " ++str m;
-      sizeMsg : String := "sizes do not match";
-      balanceMsg : String := "not balanced";
-    in [ testCase (mkTitle "size") (assertEqual sizeMsg (size testSet) testLen)
-       ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced testSet))
-       ];
+mkTests {A} (descr : TestDescr A) : List Test :=
+  case descr of
+    mkTestDescr@{testTitle; testLen; testSet} :=
+      let
+        mkTitle : String -> String
+          | m := testTitle ++str " " ++str m;
+        sizeMsg : String := "sizes do not match";
+        balanceMsg : String := "not balanced";
+      in [ testCase (mkTitle "size") (assertEqual sizeMsg (size testSet) testLen)
+         ; testCase (mkTitle "balanced") (assertTrue balanceMsg (isBalanced testSet))
+         ];
 
 type TestDescr (A : Type) :=
   mkTestDescr {
@@ -29,22 +30,22 @@ type TestDescr (A : Type) :=
     testSet : AVLTree A
   };
 
-s1-tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9];
+s1Tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9];
 
-s2-tree : AVLTree Nat := fromList [1; 3; 0; 4; 4; 8; 2];
+s2Tree : AVLTree Nat := fromList [1; 3; 0; 4; 4; 8; 2];
 
-s1 : TestDescr Nat := mkTestDescr "s1" 5 s1-tree;
+s1 : TestDescr Nat := mkTestDescr "s1" 5 s1Tree;
 
-s2 : TestDescr Nat := mkTestDescr "s2" 6 s2-tree;
+s2 : TestDescr Nat := mkTestDescr "s2" 6 s2Tree;
 
-s2-delete : TestDescr Nat :=
+s2Delete : TestDescr Nat :=
   mkTestDescr@{
     testTitle := TestDescr.testTitle s2 ++str "-delete";
     testLen := sub (TestDescr.testLen s2) 2;
     testSet := deleteMany [1; 8] (TestDescr.testSet s2)
   };
 
-s2-delete-with : TestDescr Box :=
+s2DeleteWith : TestDescr Box :=
   mkTestDescr@{
     testTitle := TestDescr.testTitle s2 ++str "-delete-with";
     testLen := sub (TestDescr.testLen s2) 2;
@@ -66,31 +67,26 @@ s4 : TestDescr Nat :=
   };
 
 tests : List Test :=
-  [ testCase "s1-member" (assertTrue "member? 3 s1" (member? 3 s1-tree))
+  [ testCase "s1-member" (assertTrue "member? 3 s1" (AVL.isMember 3 s1Tree))
   ; testCase
     "s1-s2-intersection"
-    (assertEqual
-      "intersection s1-tree s2-tree"
-      (intersection s1-tree s2-tree)
-      (fromList [1; 2; 3; 8]))
+    (assertEqual "intersection s1Tree s2Tree" (intersection s1Tree s2Tree) (fromList [1; 2; 3; 8]))
   ; testCase
     "s1-s2-difference"
-    (assertEqual "difference s1-tree s2-tree" (difference s1-tree s2-tree) (fromList [9]))
+    (assertEqual "difference s1Tree s2Tree" (difference s1Tree s2Tree) (fromList [9]))
   ; testCase
     "s1-s2-union"
-    (assertEqual "union s1-tree s2-tree" (union s1-tree s2-tree) (fromList [0; 1; 2; 3; 4; 8; 9]))
+    (assertEqual "union s1Tree s2Tree" (union s1Tree s2Tree) (fromList [0; 1; 2; 3; 4; 8; 9]))
   ; testCase "for ascending iteration"
     <| assertEqual "for iterates in ascending order" [1; 2; 3; 4]
-    <| for (acc := []) (k in fromList [3; 2; 4; 1])
-         snoc acc k
+    <| for (acc := []) (k in fromList [3; 2; 4; 1]) {snoc acc k}
   ; testCase "rfor ascending iteration"
     <| assertEqual "rfor iterates in descending order" [4; 3; 2; 1]
-    <| rfor (acc := []) (k in fromList [3; 2; 4; 1])
-         snoc acc k
+    <| rfor (acc := []) (k in fromList [3; 2; 4; 1]) {snoc acc k}
   ]
-    ++ concatMap mkTests [s1; s2; s3; s4; s2-delete];
+    ++ concatMap mkTests [s1; s2; s3; s4; s2Delete];
 
 suite : TestSuite := testSuite "AVL Set" tests;
 
 main : IO :=
-  printStringLn (pretty s1-tree) >>> printStringLn (prettyDebug s1-tree) >>> runTestSuite suite;
+  printStringLn (pretty s1Tree) >>> printStringLn (prettyDebug s1Tree) >>> runTestSuite suite;
diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix
index 6d14a639..10c5b0a3 100644
--- a/test/Test/Arb.juvix
+++ b/test/Test/Arb.juvix
@@ -6,21 +6,22 @@ import Test.QuickCheck.Arbitrary open;
 import Test.QuickCheck.Gen open;
 import Data.Random open;
 
-arbitrarySizedList {A} (size : Nat) : Arbitrary A -> Arbitrary (List A)
-  | (mkArbitrary g) :=
-    mkArbitrary
-      (mkGen
-        \ {rand :=
-          let
-            randList : StdGen -> Nat -> List A
-              | _ zero := nil
-              | r (suc n) :=
-                let
-                  rSplit : Pair StdGen StdGen := stdSplit r;
-                  r1 : StdGen := fst rSplit;
-                  r2 : StdGen := snd rSplit;
-                in Gen.run g r1 :: randList r2 n;
-          in randList rand size});
+arbitrarySizedList {A} (size : Nat) (arbitraryA : Arbitrary A) : Arbitrary (List A) :=
+  case arbitraryA of
+    mkArbitrary g :=
+      mkArbitrary
+        (mkGen
+          \ {rand :=
+            let
+              randList : StdGen -> Nat -> List A
+                | _ zero := nil
+                | r (suc n) :=
+                  let
+                    rSplit : Pair StdGen StdGen := stdSplit r;
+                    r1 : StdGen := fst rSplit;
+                    r2 : StdGen := snd rSplit;
+                  in Gen.run g r1 :: randList r2 n;
+            in randList rand size});
 
 --- Generate an arbitrary rectangular matrix
 arbitraryMatrix {A} {{arbA : Arbitrary A}} : Arbitrary (List (List A)) :=
diff --git a/test/Test/Map.juvix b/test/Test/Map.juvix
index ce4e134c..1cf9c622 100644
--- a/test/Test/Map.juvix
+++ b/test/Test/Map.juvix
@@ -14,8 +14,8 @@ tests : List Test :=
   let
     m : Map Nat String := Map.insert 2 "two" (Map.insert 1 "one" Map.empty);
     m2 : Map Nat Nat := Map.insert 3 4 (Map.insert 1 2 Map.empty);
-    assertEqListPair : List (Pair Nat Nat) -> List (Pair Nat Nat) -> Assertion
-      | actual expected := assertEqual "lists are not equal" (quickSort actual) expected;
+    assertEqListPair (actual : List (Pair Nat Nat)) (expected : List (Pair Nat Nat)) : Assertion :=
+      assertEqual "lists are not equal" (quickSort actual) expected;
   in [ testCase
        "Map.lookup missing key"
        (assertNothing (const "found a key expected to be missing") (Map.lookup 10 m))
diff --git a/test/Test/Queue.juvix b/test/Test/Queue.juvix
index c85de1e0..dee7767b 100644
--- a/test/Test/Queue.juvix
+++ b/test/Test/Queue.juvix
@@ -20,8 +20,8 @@ q4 : Queue Nat := push 4 q3;
 
 tests : List Test :=
   let
-    checkWithList : Queue Nat -> List Nat -> Assertion
-      | q q' := assertEqual "Queue should be equal" q (fromList q');
+    checkWithList (q : Queue Nat) (q' : List Nat) : Assertion :=
+      assertEqual "Queue should be equal" q (fromList q');
   in [ testCase "Queue.empty should be empty" (checkWithList q [])
      ; testCase "Queue.push should add an element" (checkWithList q1 [1])
      ; testCase "Queue.push first element should be first pushed" (checkWithList q2 [1; 2])
diff --git a/test/Test/UnbalancedSet.juvix b/test/Test/UnbalancedSet.juvix
index 53c62cfe..3a54bb03 100644
--- a/test/Test/UnbalancedSet.juvix
+++ b/test/Test/UnbalancedSet.juvix
@@ -17,13 +17,13 @@ tests : List Test :=
        (assertEqual "unexpected size" (Set.length s) 3)
      ; testCase
        "Set.to-list computes the expected members"
-       (assertEqual "unexpected memebrs" (quickSort (Set.to-list s)) [1; 2; 3])
+       (assertEqual "unexpected memebrs" (quickSort (Set.toList s)) [1; 2; 3])
      ; testCase
        "Set.member? computes true for expected member"
-       (assertTrue "expected member is not present" (Set.member? 1 s))
+       (assertTrue "expected member is not present" (Set.isMember 1 s))
      ; testCase
        "Set.member? computes false for unexpected member"
-       (assertFalse "unexpected member is present" (Set.member? 0 s))
+       (assertFalse "unexpected member is present" (Set.isMember 0 s))
      ; testCase "setInSet has length 1" (assertEqual "unexpected size" (Set.length setInSet) 1)
      ];
 
diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml
index b565a8e3..b8049268 100644
--- a/test/juvix.lock.yaml
+++ b/test/juvix.lock.yaml
@@ -2,27 +2,27 @@
 # Do not edit this file manually.
 
 version: 2
-checksum: 05003064be8ff630775c22735af69a82ddd4ac04fdd3ad6aa0c3f01867777225
+checksum: fbbd33d3d068b3369d271021b23b0407838642655173d086f1c81ead9bb338c8
 dependencies:
 - path: ../
   dependencies: []
 - git:
     name: anoma_juvix-quickcheck
-    ref: b398d3cd58f0a7fb9be24d57fc5b3d82f31de555
+    ref: 4242b864714f98947753544ea1b2cb435f6473d3
     url: https://github.com/anoma/juvix-quickcheck
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: af72f25057217619a03b7a5114000d02d0abed31
+      ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []
 - git:
     name: anoma_juvix-test
-    ref: 3103c41e055eb9018a851fd3688cd608cad8f55d
+    ref: 85811914324b082549cb1f500323884442fc793c
     url: https://github.com/anoma/juvix-test
   dependencies:
   - git:
       name: anoma_juvix-stdlib
-      ref: 615a02c8107076ca9661c5234d41792be91a5104
+      ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6
       url: https://github.com/anoma/juvix-stdlib
     dependencies: []