diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix
index 2b5cadc3..4da9aab2 100644
--- a/Stdlib/Data/BinaryTree.juvix
+++ b/Stdlib/Data/BinaryTree.juvix
@@ -19,6 +19,6 @@ fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B :=
       | (node l a r) := f a (go acc l) (go acc r);
   in go acc tree;
 
-length {A} (tree : BinaryTree A) : Nat := fold \ {_ l r := 1 + l + r} 0 tree;
+length {A} (tree : BinaryTree A) : Nat := fold \{_ l r := 1 + l + r} 0 tree;
 
-toList {A} (tree : BinaryTree A) : List A := fold \ {e ls rs := e :: ls ++ rs} nil tree;
+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 6aa14b87..50423dc5 100644
--- a/Stdlib/Data/Bool.juvix
+++ b/Stdlib/Data/Bool.juvix
@@ -9,7 +9,7 @@ import Stdlib.Trait.Show open;
 
 {-# specialize: true, inline: case #-}
 instance
-boolEqI : Eq Bool :=
+eqBoolI : Eq Bool :=
   mkEq@{
     eq (x y : Bool) : Bool :=
       case x, y of
@@ -20,7 +20,7 @@ boolEqI : Eq Bool :=
 
 {-# specialize: true, inline: case #-}
 instance
-boolOrdI : Ord Bool :=
+ordBoolI : Ord Bool :=
   mkOrd@{
     cmp (x y : Bool) : Ordering :=
       case x, y of
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index f415483c..99f880dc 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/Stdlib/Data/List/Base.juvix
@@ -68,11 +68,17 @@ filter {A} (predicate : A -> Bool) : (list : List A) -> List A
       | else := filter predicate hs;
 
 --- 𝒪(𝓃). Returns the length of the ;List;.
-length {A} (l : List A) : Nat := listFor (acc := zero) (_ in l) {suc acc};
+length {A} (list : List A) : Nat :=
+  listFor (acc := zero) (_ in list) {
+    suc acc
+  };
 
 --- 𝒪(𝓃). Returns the given ;List; in reverse order.
 {-# isabelle-function: {name: "rev"} #-}
-reverse {A} (l : List A) : List A := listFor (acc := nil) (x in l) {x :: acc};
+reverse {A} (list : List A) : List A :=
+  listFor (acc := nil) (x in list) {
+    x :: acc
+  };
 
 --- Returns a ;List; of length resultLength where every element is the given value.
 replicate {A} : (resultLength : Nat) -> (value : A) -> List A
@@ -188,13 +194,13 @@ isEmpty {A} (list : List A) : Bool :=
 --- 𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function
 --- to each pair of elements from the input lists.
 {-# specialize: [1] #-}
-zipWith {A B C} (fun : A -> B -> C) : (listA : List A) -> (listB : List B) -> List C
+zipWith {A B C} (fun : A -> B -> C) : (list1 : List A) -> (list2 : List B) -> List C
   | nil _ := nil
   | _ nil := nil
   | (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} : (listA : List A) -> (listB : List B) -> List (Pair A B)
+zip {A B} : (list1 : List A) -> (list2 : List B) -> List (Pair A B)
   | nil _ := nil
   | _ nil := nil
   | (x :: xs) (y :: ys) := (x, y) :: zip xs ys;
@@ -225,7 +231,7 @@ quickSort {A} {{Ord A}} (list : List A) : List A :=
     go : List A -> List A
       | nil := nil
       | xs@(_ :: nil) := xs
-      | (x :: xs) := case partition \ {y := y < x} xs of l1, l2 := go l1 ++ x :: go l2;
+      | (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;.
@@ -243,5 +249,5 @@ concatMap {A B} (fun : A -> List B) (list : List A) : List B := flatten (listMap
 --- 𝒪(𝓃 * 𝓂). Transposes a ;List; of ;List;s interpreted as a matrix.
 transpose {A} : (listOfLists : List (List A)) -> List (List A)
   | nil := nil
-  | (xs :: nil) := listMap λ {x := x :: nil} xs
+  | (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 d441d85e..63c89171 100644
--- a/Stdlib/Data/Map.juvix
+++ b/Stdlib/Data/Map.juvix
@@ -6,7 +6,7 @@ import Stdlib.Data.List open;
 import Stdlib.Data.Nat open;
 import Stdlib.Data.Bool open;
 
-import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Functor open using {Functor; mkFunctor; map as fmap};
 import Stdlib.Trait.Foldable open hiding {foldr; foldl};
 import Stdlib.Trait.Ord open;
 
@@ -57,122 +57,167 @@ insertWith
         binding := mkBinding key value;
       in mkMap (Set.insertWith fun' binding tree);
 
---- 𝒪(log 𝓃). Inserts an element into a ;Map; at a given key.
+--- 𝒪(log 𝓃). Inserts a new `key` and `value` into `map`. If `key` is already
+--- present in `map`, the associated value is replaced with the supplied
+--- `value`.
 {-# inline: true #-}
-insert {Key Value : Type} {{Ord Key}} : Key -> Value -> Map Key Value -> Map Key Value :=
-  insertWith \ {old new := new};
+insert
+  {Key Value : Type} {{Ord Key}} (key : Key) (elem : Value) (map : Map Key Value) : Map Key Value :=
+  insertWith (flip const) key elem map;
 
---- 𝒪(log 𝓃). Queries whether a given key is in a ;Map;.
+--- 𝒪(log 𝓃). Queries whether a given `key` is in `map`.
 {-# specialize: [1] #-}
-lookup {Key Value} {{Ord Key}} (lookupKey : Key) (container : Map Key Value) : Maybe Value :=
-  case container of mkMap s := map value (Set.lookupWith key lookupKey s);
+lookup {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Maybe Value :=
+  case map of mkMap s := fmap value (Set.lookupWith Binding.key key s);
 
---- 𝒪(log 𝓃). Queries whether a given key is in a ;Map;.
+--- 𝒪(log 𝓃). Queries whether a given `key` is in `map`.
 {-# specialize: [1] #-}
-isMember {Key Value} {{Ord Key}} (key : Key) (container : Map Key Value) : Bool :=
-  isJust (lookup key container);
+isMember {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Bool :=
+  isJust (lookup key map);
 
 {-# specialize: [1, f] #-}
 fromListWithKey
   {Key Value}
   {{Ord Key}}
-  (f : Key -> Value -> Value -> Value)
-  (xs : List (Pair Key Value))
-  : Map Key Value := for (acc := empty) (k, v in xs) {insertWith (f k) k v acc};
+  (fun : Key -> Value -> Value -> Value)
+  (list : List (Pair Key Value))
+  : Map Key Value :=
+  for (acc := empty) (k, v in list) {
+    insertWith (fun k) k v acc
+  };
 
 {-# inline: true #-}
 fromListWith
   {Key Value}
   {{Ord Key}}
-  (f : Value -> Value -> Value)
-  (xs : List (Pair Key Value))
-  : Map Key Value := fromListWithKey (const f) xs;
+  (fun : Value -> Value -> Value)
+  (list : List (Pair Key Value))
+  : Map Key Value := fromListWithKey (const fun) list;
 
 {-# inline: true #-}
-fromList {Key Value} {{Ord Key}} : List (Pair Key Value) -> Map Key Value :=
-  fromListWith λ {old new := new};
+fromList {Key Value} {{Ord Key}} (list : List (Pair Key Value)) : Map Key Value :=
+  fromListWith (flip const) list;
 
-toList {Key Value} (container : Map Key Value) : List (Pair Key Value) :=
-  case container of mkMap s := map (x in Set.toList s) {toPair x};
+toList {Key Value} (map : Map Key Value) : List (Pair Key Value) :=
+  case map of
+    mkMap s :=
+      fmap (x in Set.toList s) {
+        toPair x
+      };
 
 {-# specialize: [1, f] #-}
-fromSet {Key Value} {{Ord Key}} (f : Key -> Value) (set : Set Key) : Map Key Value :=
-  for (acc := empty) (k in set) {insert k (f k) acc};
+fromSet {Key Value} {{Ord Key}} (fun : Key -> Value) (set : Set Key) : Map Key Value :=
+  for (acc := empty) (k in set) {
+    insert k (fun k) acc
+  };
 
 --- 𝒪(1). Checks if a ;Map; is empty.
 {-# inline: true #-}
-isEmpty {Key Value} (container : Map Key Value) : Bool :=
-  case container of mkMap s := Set.isEmpty s;
+isEmpty {Key Value} (map : Map Key Value) : Bool := case map of mkMap s := Set.isEmpty s;
 
 --- 𝒪(𝓃). Returns the number of elements of a ;Map;.
 {-# inline: true #-}
-size {Key Value} (container : Map Key Value) : Nat := case container of mkMap s := Set.size s;
+size {Key Value} (map : Map Key Value) : Nat := case map of mkMap s := Set.size s;
 
---- 𝒪(log 𝓃). Removes a key assignment from a ;Map;.
+--- 𝒪(log 𝓃). Removes `key` assignment from `map`.
 {-# inline: true #-}
-delete {Key Value} {{Ord Key}} (deleteKey : Key) (container : Map Key Value) : Map Key Value :=
-  case container of mkMap s := mkMap (Set.deleteWith key deleteKey s);
+delete {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Map Key Value :=
+  case map of mkMap s := mkMap (Set.deleteWith Binding.key key s);
 
-keys {Key Value} (container : Map Key Value) : List Key :=
-  case container of mkMap s := map (x in Set.toList s) {key x};
+keys {Key Value} (map : Map Key Value) : List Key :=
+  case map of
+    mkMap s :=
+      fmap (x in Set.toList s) {
+        key x
+      };
 
-values {Key Value} (container : Map Key Value) : List Value :=
-  case container of mkMap s := map (x in Set.toList s) {value x};
+values {Key Value} (map : Map Key Value) : List Value :=
+  case map of
+    mkMap s :=
+      fmap (x in Set.toList s) {
+        value x
+      };
 
-keySet {Key Value} {{Ord Key}} (container : Map Key Value) : Set Key :=
-  case container of mkMap s := Set.map (x in s) {key x};
+keySet {Key Value} {{Ord Key}} (map : Map Key Value) : Set Key :=
+  case map of
+    mkMap s :=
+      Set.map (x in s) {
+        key x
+      };
 
-valueSet {Key Value} {{Ord Value}} (container : Map Key Value) : Set Value :=
-  case container of mkMap s := Set.map (x in s) {value x};
+valueSet {Key Value} {{Ord Value}} (map : Map Key Value) : Set Value :=
+  case map of
+    mkMap s :=
+      Set.map (x in s) {
+        value x
+      };
 
 {-# specialize: [f] #-}
 mapValuesWithKey
-  {Key Value1 Value2} (f : Key -> Value1 -> Value2) (container : Map Key Value1) : Map Key Value2 :=
-  case container of
-    mkMap s := mkMap (Set.Internal.unsafeMap \ {(mkBinding k v) := mkBinding k (f k v)} s);
+  {Key Value1 Value2} (fun : Key -> Value1 -> Value2) (map : Map Key Value1) : Map Key Value2 :=
+  case map of
+    mkMap s := mkMap (Set.Internal.unsafeMap \{(mkBinding k v) := mkBinding k (fun k v)} s);
 
 {-# inline: true #-}
-mapValues
-  {Key Value1 Value2} (f : Value1 -> Value2) (container : Map Key Value1) : Map Key Value2 :=
-  mapValuesWithKey (const f) container;
+mapValues {Key Value1 Value2} (fun : Value1 -> Value2) (map : Map Key Value1) : Map Key Value2 :=
+  mapValuesWithKey (const fun) map;
 
 {-# inline: true #-}
 singleton {Key Value} {{Ord Key}} (key : Key) (value : Value) : Map Key Value :=
   insert key value empty;
 
 {-# inline: true #-}
-foldr
-  {Key Value Acc} (f : Key -> Value -> Acc -> Acc) (acc : Acc) (container : Map Key Value) : Acc :=
-  case container of mkMap s := rfor (acc := acc) (x in s) {f (key x) (value x) acc};
+foldr {Key Value Acc} (fun : Key -> Value -> Acc -> Acc) (acc : Acc) (map : Map Key Value) : Acc :=
+  case map of
+    mkMap s :=
+      rfor (acc := acc) (x in s) {
+        fun (key x) (value x) acc
+      };
 
 {-# inline: true #-}
-foldl
-  {Key Value Acc} (f : Acc -> Key -> Value -> Acc) (acc : Acc) (container : Map Key Value) : Acc :=
-  case container of mkMap s := for (acc := acc) (x in s) {f acc (key x) (value x)};
+foldl {Key Value Acc} (fun : Acc -> Key -> Value -> Acc) (acc : Acc) (map : Map Key Value) : Acc :=
+  case map of
+    mkMap s :=
+      for (acc := acc) (x in s) {
+        fun acc (key x) (value x)
+      };
 
 syntax iterator all {init := 0; range := 1};
---- 𝒪(𝓃). Returns ;true; if all key-element pairs in the ;Map; satisfy the predicate.
+--- 𝒪(𝓃). Returns ;true; if all key-value pairs in `map` satisfy `predicate`.
 {-# inline: true #-}
-all {Key Value} (predicate : Key -> Value -> Bool) (container : Map Key Value) : Bool :=
-  case container of mkMap s := Set.all (x in s) {predicate (key x) (value x)};
+all {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
+  case map of
+    mkMap s :=
+      Set.all (x in s) {
+        predicate (key x) (value x)
+      };
 
 syntax iterator any {init := 0; range := 1};
---- 𝒪(𝓃). Returns ;true; if some key-element pair in the ;Map; satisfies the predicate.
+--- 𝒪(𝓃). Returns ;true; if some key-value pair in `map` satisfies `predicate`.
 {-# inline: true #-}
-any {Key Value} (predicate : Key -> Value -> Bool) (container : Map Key Value) : Bool :=
-  case container of mkMap s := Set.any (x in s) {predicate (key x) (value x)};
+any {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
+  case map of
+    mkMap s :=
+      Set.any (x in s) {
+        predicate (key x) (value x)
+      };
 
 syntax iterator filter {init := 0; range := 1};
---- 𝒪(n log n). Returns a ;Map; containing all key-element pairs of the given
---- map container that satisfy the predicate.
+--- 𝒪(n log n). Returns a ;Map; containing all key-value pairs of `map` that
+--- satisfy `predicate`.
 {-# inline: true #-}
 filter
   {Key Value}
   {{Ord Key}}
   (predicate : Key -> Value -> Bool)
-  (container : Map Key Value)
+  (map : Map Key Value)
   : Map Key Value :=
-  case container of mkMap s := mkMap (Set.filter (x in s) {predicate (key x) (value x)});
+  case map of
+    mkMap s :=
+      mkMap
+        (Set.filter (x in s) {
+          predicate (key x) (value x)
+        });
 
 syntax iterator partition {init := 0; range := 1};
 {-# inline: true #-}
@@ -180,18 +225,21 @@ partition
   {Key Value}
   {{Ord Key}}
   (predicate : Key -> Value -> Bool)
-  (container : Map Key Value)
+  (map : Map Key Value)
   : Pair (Map Key Value) (Map Key Value) :=
-  case container of
+  case map of
     mkMap s :=
-      case Set.partition (x in s) {predicate (key x) (value x)} of
-        left, right := mkMap left, mkMap right;
+      case
+        Set.partition (x in s) {
+          predicate (key x) (value x)
+        }
+      of left, right := mkMap left, mkMap right;
 
 {-# specialize: true, inline: case #-}
 instance
 functorMapI {Key} : Functor (Map Key) :=
   mkFunctor@{
-    map {A B} (f : A -> B) (container : Map Key A) : Map Key B := mapValues f container
+    map {A B} (fun : A -> B) (container : Map Key A) : Map Key B := mapValues fun container
   };
 
 {-# specialize: true, inline: case #-}
@@ -199,12 +247,12 @@ instance
 foldableMapI {Key Value} : Foldable (Map Key Value) (Pair Key Value) :=
   mkFoldable@{
     {-# inline: true #-}
-    for {B} (f : B -> Pair Key Value -> B) (acc : B) (container : Map Key Value) : B :=
-      foldl \ {a k v := f a (k, v)} acc container;
+    for {B} (f : B -> Pair Key Value -> B) (acc : B) (map : Map Key Value) : B :=
+      foldl \{a k v := f a (k, v)} acc map;
 
     {-# inline: true #-}
-    rfor {B} (f : B -> Pair Key Value -> B) (acc : B) (container : Map Key Value) : B :=
-      foldr \ {k v a := f a (k, v)} acc container
+    rfor {B} (f : B -> Pair Key Value -> B) (acc : B) (map : Map Key Value) : B :=
+      foldr \{k v a := f a (k, v)} acc map
   };
 
 instance
diff --git a/Stdlib/Data/Pair/Base.juvix b/Stdlib/Data/Pair/Base.juvix
index 39a41eeb..dae78ccc 100644
--- a/Stdlib/Data/Pair/Base.juvix
+++ b/Stdlib/Data/Pair/Base.juvix
@@ -9,10 +9,10 @@ builtin pair
 type Pair (A B : Type) := , : A → B → Pair 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;
+uncurry {A B C} (fun : A -> B -> C) (pair : Pair A B) : C := case pair of a, b := fun a b;
 
 --- 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);
+curry {A B C} (fun : Pair A B -> C) (a : A) (b : B) : C := fun (a, b);
 
 --- Projects the first component of a tuple.
 fst {A B} (pair : Pair A B) : A := case pair of a, _ := a;
@@ -24,10 +24,10 @@ snd {A B} (pair : Pair A B) : B := case pair of _, b := b;
 swap {A B} (pair : Pair A B) : Pair B A := case pair of a, b := b, a;
 
 --- 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;
+first {A B A'} (fun : A -> A') (pair : Pair A B) : Pair A' B := case pair of a, b := fun a, 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;
+second {A B B'} (fun : B -> B') (pair : Pair A B) : Pair A B' := case pair of a, b := a, fun 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;
+both {A B} (fun : A -> B) (pair : Pair A A) : Pair B B := case pair of a, b := fun a, fun b;
diff --git a/Stdlib/Data/Queue/Base.juvix b/Stdlib/Data/Queue/Base.juvix
index 14952f36..54271825 100644
--- a/Stdlib/Data/Queue/Base.juvix
+++ b/Stdlib/Data/Queue/Base.juvix
@@ -66,7 +66,9 @@ push {A} (x : A) (queue : Queue A) : Queue A :=
 
 --- 𝒪(n). Adds a list of elements to the end of the ;Queue;.
 pushMany {A} (list : List A) (queue : Queue A) : Queue A :=
-  for (acc := queue) (x in list) {push x acc};
+  for (acc := queue) (x in list) {
+    push x acc
+  };
 
 --- 𝒪(n). Build a ;Queue; from a ;List;.
 fromList {A} (list : List A) : Queue A := pushMany list empty;
diff --git a/Stdlib/Data/Range.juvix b/Stdlib/Data/Range.juvix
index 530e048e..b825ecbd 100644
--- a/Stdlib/Data/Range.juvix
+++ b/Stdlib/Data/Range.juvix
@@ -31,7 +31,7 @@ syntax operator step step;
 
 --- `x to y step s` is the range [x, x + s, ..., y]
 {-# inline: always #-}
-step {N} (range : Range N) (stp : N) : StepRange N := mkStepRange range stp;
+step {N} (range : Range N) (step : N) : StepRange N := mkStepRange range step;
 
 -- This instance assumes that `low <= high`.
 {-# specialize: true, inline: case #-}
@@ -39,26 +39,26 @@ instance
 foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
   mkFoldable@{
     {-# specialize: [1, 3] #-}
-    for {B : Type} (f : B -> N -> B) (initialValue : B) : Range N -> B
+    for {B : Type} (fun : B -> N -> B) (initialValue : B) : Range N -> B
       | (mkRange low high) :=
         let
-          {-# specialize-by: [f, high] #-}
+          {-# specialize-by: [fun, high] #-}
           terminating
           go (acc : B) (next : N) : B :=
             if
-              | next == high := f acc next
-              | else := go (f acc next) (next + 1);
+              | next == high := fun acc next
+              | else := go (fun acc next) (next + 1);
         in go initialValue low;
     {-# specialize: [1, 3] #-}
-    rfor {B : Type} (f : B -> N -> B) (initialValue : B) : Range N -> B
+    rfor {B : Type} (fun : B -> N -> B) (initialValue : B) : Range N -> B
       | (mkRange low high) :=
         let
-          {-# specialize-by: [f, high] #-}
+          {-# specialize-by: [fun, high] #-}
           terminating
           go (next : N) : B :=
             if
-              | next == high := f initialValue next
-              | else := f (go (next + 1)) next;
+              | next == high := fun initialValue next
+              | else := fun (go (next + 1)) next;
         in go low
   };
 
@@ -68,25 +68,25 @@ instance
 foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
   mkFoldable@{
     {-# specialize: [1, 3] #-}
-    for {B : Type} (f : B -> N -> B) (initialValue : B) : StepRange N -> B
+    for {B : Type} (fun : B -> N -> B) (initialValue : B) : StepRange N -> B
       | (mkStepRange (mkRange low high) step) :=
         let
-          {-# specialize-by: [f, high, step] #-}
+          {-# specialize-by: [fun, high, step] #-}
           terminating
           go (acc : B) (next : N) : B :=
             if
               | next > high := acc
-              | else := go (f acc next) (next + step);
+              | else := go (fun acc next) (next + step);
         in go initialValue low;
     {-# specialize: [1, 3] #-}
-    rfor {B : Type} (f : B -> N -> B) (initialValue : B) : StepRange N -> B
+    rfor {B : Type} (fun : B -> N -> B) (initialValue : B) : StepRange N -> B
       | (mkStepRange (mkRange low high) step) :=
         let
-          {-# specialize-by: [f, high, step] #-}
+          {-# specialize-by: [fun, high, step] #-}
           terminating
           go (next : N) : B :=
             if
-              | next <= high := f (go (next + step)) next
+              | next <= high := fun (go (next + step)) next
               | else := initialValue;
         in go low
   };
diff --git a/Stdlib/Data/Result/Base.juvix b/Stdlib/Data/Result/Base.juvix
index 3d98ffe3..d3ba7865 100644
--- a/Stdlib/Data/Result/Base.juvix
+++ b/Stdlib/Data/Result/Base.juvix
@@ -26,16 +26,16 @@ handleResult
 --- Apply a function f to the ;error; value of a Result.
 mapError
   {Value Error1 Error2}
-  (f : Error1 -> Error2)
+  (fun : Error1 -> Error2)
   (result : Result Error1 Value)
-  : Result Error2 Value := handleResult (f >> error) ok result;
+  : Result Error2 Value := handleResult (fun >> error) ok result;
 
 --- Apply a function f to the ;ok; value of a Result.
 mapOk
   {Error Value1 Value2}
-  (f : Value1 -> Value2)
+  (fun : Value1 -> Value2)
   (result : Result Error Value1)
-  : Result Error Value2 := handleResult error (f >> ok) result;
+  : Result Error Value2 := handleResult error (fun >> ok) result;
 
 --- Return ;true; if the value is an ;error;, otherwise ;false;.
 isError {Error Value} (result : Result Error Value) : Bool :=
diff --git a/Stdlib/Data/Set/AVL.juvix b/Stdlib/Data/Set/AVL.juvix
index 9e837825..d66d140d 100644
--- a/Stdlib/Data/Set/AVL.juvix
+++ b/Stdlib/Data/Set/AVL.juvix
@@ -31,29 +31,31 @@ type AVLTree (A : Type) :=
       right : AVLTree A
     };
 
---- 𝒪(1) Retrieves the height of an ;AVLTree;. The height is the distance from
---- the root to the deepest child.
-height {A} (tree : AVLTree A) : Nat :=
-  case tree of
-    | empty := 0
-    | node@{height} := height;
-
 module Internal;
+  --- 𝒪(1) Retrieves the height of an ;AVLTree;. The height is the distance from
+  --- the root to the deepest child.
+  height {A} (set : AVLTree A) : Nat :=
+    case set of
+      | empty := 0
+      | node@{height} := height;
+
   --- 𝒪(n). Maps a function over an ;AVLTree;. Does not check if
   --- after mapping the order of the elements is preserved. It is the
   --- responsibility of the caller to ensure that `f` preserves the ordering.
-  unsafeMap {A B} (f : A -> B) (tree : AVLTree A) : AVLTree B :=
+  unsafeMap {A B} (f : A -> B) (set : AVLTree A) : AVLTree B :=
     let
       go : AVLTree A -> AVLTree B
         | empty := empty
         | node@{element; height; left; right} :=
-          -- TODO: we cannot use record creation syntax here because of a bug in the type-checker (https://github.com/anoma/juvix/issues/3112)
+          -- TODO: use record creation syntax here once recursive definition
+            -- parsing is fixed (https://github.com/anoma/juvix/issues/2968,
+            -- https://github.com/anoma/juvix/issues/3112)
             node
             (f element)
             height
             (go left)
             (go right);
-    in go tree;
+    in go set;
 
   type BalanceFactor :=
     | --- Left child is higher.
@@ -63,8 +65,8 @@ module Internal;
     | --- Right child is higher.
       LeanRight;
 
-  diffFactor {A} (tree : AVLTree A) : Int :=
-    case tree of
+  diffFactor {A} (set : AVLTree A) : Int :=
+    case set of
       | empty := 0
       | node@{left; right} := intSubNat (height right) (height left);
 
@@ -80,9 +82,9 @@ module Internal;
 
   --- 𝒪(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 :=
+  balanceFactor {A} (set : AVLTree A) : BalanceFactor :=
     -- We avoid `diffFactor` here for efficiency.
-    case tree of
+    case set of
       | empty := LeanNone
       | node@{left; right} := balanceFactor' left right;
 
@@ -91,42 +93,48 @@ module Internal;
     node value (1 + max (height left) (height right)) left right;
 
   --- 𝒪(1). Left rotation.
-  rotateLeft {A} (tree : AVLTree A) : AVLTree A :=
-    case tree of
+  rotateLeft {A} (set : AVLTree A) : AVLTree A :=
+    case set of
       | node x _ a (node z _ b c) := mkNode z (mkNode x a b) c
       | n := n;
 
   --- 𝒪(1). Right rotation.
-  rotateRight {A} (tree : AVLTree A) : AVLTree A :=
-    case tree of
+  rotateRight {A} (set : AVLTree A) : AVLTree A :=
+    case set 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} (tree : AVLTree A) : AVLTree A :=
-    case tree of
+  balance {A} (set : AVLTree A) : AVLTree A :=
+    case set 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
+              | _ := rotateLeft set
             }
           | LeanLeft :=
             case balanceFactor left of {
               | LeanRight := rotateRight (mkNode element (rotateLeft left) right)
-              | _ := rotateRight tree
+              | _ := rotateRight set
             }
-          | LeanNone := tree;
+          | LeanNone := set;
+
+  --- 𝒪(𝓃). Checks the ;AVLTree; height invariant. I.e. that
+  --- every two children do not differ on height by more than 1.
+  isBalanced {A} : (set : AVLTree A) -> Bool
+    | empty := true
+    | set@node@{left; right} := isBalanced left && isBalanced right && abs (diffFactor set) <= 1;
 end;
 
 open Internal;
 
---- 𝒪(log 𝓃). Lookup a member from the ;AVLTree; using a projection function.
+--- 𝒪(log 𝓃). Lookup a member from the set using a projection function.
 --- 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 :=
+lookupWith {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (set : AVLTree A) : Maybe A :=
   let
     {-# specialize-by: [order, fun] #-}
     go : AVLTree A -> Maybe A
@@ -136,23 +144,23 @@ lookupWith {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (tree : AVLTree A)
           | LessThan := go left
           | GreaterThan := go right
           | Equal := just element;
-  in go tree;
+  in go set;
 
---- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
+--- 𝒪(log 𝓃). Queries whether `elem` is in `set`.
 {-# specialize: [1] #-}
-lookup {A} {{Ord A}} (elem : A) (tree : AVLTree A) : Maybe A := lookupWith id elem tree;
+lookup {A} {{Ord A}} (elem : A) (set : AVLTree A) : Maybe A := lookupWith id elem set;
 
---- 𝒪(log 𝓃). Queries whether an element is in an ;AVLTree;.
+--- 𝒪(log 𝓃). Queries whether `elem` is in `set`.
 {-# specialize: [1] #-}
-isMember {A} {{Ord A}} (elem : A) (tree : AVLTree A) : Bool := isJust (lookupWith id elem tree);
+isMember {A} {{Ord A}} (elem : A) (set : AVLTree A) : Bool := isJust (lookupWith id elem set);
 
---- 𝒪(log 𝓃). Inserts an element elem into and ;AVLTree; using a function to
+--- 𝒪(log 𝓃). Inserts an element `elem` into `set` using a function to
 --- deduplicate entries.
 ---
 --- Assumption: If a1 == a2 then fun a1 a2 == a1 == a2
 --- where == comes from Ord a.
 {-# specialize: [1, 2] #-}
-insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (tree : AVLTree A) : AVLTree A :=
+insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (set : AVLTree A) : AVLTree A :=
   let
     {-# specialize-by: [order, fun] #-}
     go : AVLTree A -> AVLTree A
@@ -162,22 +170,22 @@ insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (tree : AVLTree
           | 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;
+  in go set;
 
---- 𝒪(log 𝓃). Inserts an element into an ;AVLTree;.
+--- 𝒪(log 𝓃). Inserts `elem` into `set`.
 {-# specialize: [1] #-}
-insert {A} {{Ord A}} (elem : A) (tree : AVLTree A) : AVLTree A := insertWith (flip const) elem tree;
+insert {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree A := insertWith (flip const) elem set;
 
---- 𝒪(log 𝓃). Removes the minimum element from an ;AVLTree;.
+--- 𝒪(log 𝓃). Removes the minimum element from `set`.
 {-# specialize: [1] #-}
-deleteMin {A} {{Ord A}} : (tree : AVLTree A) -> Maybe (Pair A (AVLTree A))
+deleteMin {A} {{Ord A}} : (set : 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.
+--- 𝒪(log 𝓃). Removes an element `elem` from `set` based on a projected comparison value.
 ---
 --- Assumption Ord A and Ord B are compatible: Given a1 a2, A then (fun a1 == fun a2) == (a1 == a2)
 {-# specialize: [1, 2, 3] #-}
@@ -187,7 +195,7 @@ deleteWith
   {{orderB : Ord B}}
   (fun : A -> B)
   (elem : B)
-  (tree : AVLTree A)
+  (set : AVLTree A)
   : AVLTree A :=
   let
     {-# specialize-by: [orderA, orderB, fun] #-}
@@ -204,67 +212,67 @@ deleteWith
                 case deleteMin right of
                   | nothing := left
                   | just (minRight, right') := balance (mkNode minRight left right');
-  in go tree;
+  in go set;
 
---- 𝒪(log 𝓃). Removes an element from an ;AVLTree;.
+--- 𝒪(log 𝓃). Removes `elem` from `set`.
 {-# specialize: [1] #-}
-delete {A} {{Ord A}} : A -> AVLTree A -> AVLTree A := deleteWith id;
+delete {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree A := deleteWith id elem set;
 
---- 𝒪(log 𝓃). Returns the minimum element of the ;AVLTree;.
-lookupMin {A} : AVLTree A -> Maybe A
+--- 𝒪(log 𝓃). Returns the minimum element of `set`.
+lookupMin {A} : (set : AVLTree A) -> Maybe A
   | empty := nothing
   | (node y _ empty empty) := just y
   | (node _ _ empty r) := lookupMin r
   | (node _ _ l _) := lookupMin l;
 
---- 𝒪(log 𝓃). Returns the maximum element of the ;AVLTree;.
-lookupMax {A} : AVLTree A -> Maybe A
+--- 𝒪(log 𝓃). Returns the maximum element of `set`.
+lookupMax {A} : (set : AVLTree A) -> Maybe A
   | empty := nothing
   | (node y _ empty empty) := just y
   | (node _ _ l empty) := lookupMax l
   | (node _ _ _ r) := lookupMax r;
 
---- 𝒪(𝒹 log 𝓃). Deletes elements from an ;AVLTree;.
+--- 𝒪(𝒹 log 𝓃). Deletes elements from `set`.
 {-# specialize: [1] #-}
-deleteMany {A} {{Ord A}} : List A -> AVLTree A -> AVLTree A := deleteManyWith id;
+deleteMany {A} {{Ord A}} (toDelete : List A) (set : AVLTree A) : AVLTree A :=
+  deleteManyWith id toDelete set;
 
---- 𝒪(𝒹 log 𝓃). Deletes elements from an ;AVLTree; based on a projected comparison value.
+--- 𝒪(𝒹 log 𝓃). Deletes elements from `set` based on a projected comparison value.
 ---
 --- 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} : (tree : AVLTree A) -> Bool
-  | empty := true
-  | tree@node@{left; right} := isBalanced left && isBalanced right && abs (diffFactor tree) <= 1;
+  {A B} {{Ord A}} {{Ord B}} (fun : A -> B) (toDelete : List B) (set : AVLTree A) : AVLTree A :=
+  for (acc := set) (x in toDelete) {
+    deleteWith fun x acc
+  };
 
---- 𝒪(𝓃 log 𝓃). Create an ;AVLTree; from an unsorted ;List;.
+--- 𝒪(𝓃 log 𝓃). Create a set from an unsorted ;List;.
 {-# specialize: [1] #-}
-fromList {A} {{Ord A}} (list : List A) : AVLTree A := for (acc := empty) (x in list) {insert x acc};
+fromList {A} {{Ord A}} (list : List A) : AVLTree A :=
+  for (acc := empty) (x in list) {
+    insert x acc
+  };
 
---- 𝒪(1). Checks if an ;AVLTree; is empty.
+--- 𝒪(1). Checks if `set` is empty.
 {-# inline: true #-}
-isEmpty {A} (tree : AVLTree A) : Bool :=
-  case tree of
+isEmpty {A} (set : AVLTree A) : Bool :=
+  case set of
     | empty := true
     | node@{} := false;
 
---- 𝒪(𝓃). Returns the number of elements of an ;AVLTree;.
-size {A} : AVLTree A -> Nat
+--- 𝒪(𝓃). Returns the number of elements of `set`.
+size {A} : (set : AVLTree A) -> Nat
   | empty := 0
   | node@{left; right} := 1 + size left + size right;
 
 {-# specialize: [1] #-}
-foldr {A B} (fun : A -> B -> B) (acc : B) : AVLTree A -> B
+foldr {A B} (fun : A -> B -> B) (acc : B) : (set : AVLTree A) -> B
   | empty := acc
   | node@{element; left; right} := foldr fun (fun element (foldr fun acc right)) left;
 
 {-# specialize: [1] #-}
-foldl {A B} (fun : B -> A -> B) (acc : B) : AVLTree A -> B
+foldl {A B} (fun : B -> A -> B) (acc : B) : (set : AVLTree A) -> B
   | empty := acc
   | node@{element; left; right} := foldl fun (fun (foldl fun acc left) element) right;
 
@@ -273,110 +281,124 @@ instance
 polymorphicFoldableAVLTreeI : Polymorphic.Foldable AVLTree :=
   Polymorphic.mkFoldable@{
     {-# inline: true #-}
-    for {A B} (f : B -> A -> B) (acc : B) (tree : AVLTree A) : B := foldl f acc tree;
+    for {A B} (f : B -> A -> B) (acc : B) (set : AVLTree A) : B := foldl f acc set;
     {-# inline: true #-}
-    rfor {A B} (f : B -> A -> B) (acc : B) (tree : AVLTree A) : B := foldr (flip f) acc tree
+    rfor {A B} (f : B -> A -> B) (acc : B) (set : AVLTree A) : B := foldr (flip f) acc set
   };
 
 {-# specialize: true, inline: true #-}
 instance
 foldableAVLTreeI {A} : Foldable (AVLTree A) A := fromPolymorphicFoldable;
 
---- 𝒪(n). Returns the elements of an ;AVLTree; in ascending order.
-toList {A} (tree : AVLTree A) : List A := rfor (acc := nil) (x in tree) {x :: acc};
+--- 𝒪(n). Returns the elements of `set` in ascending order.
+toList {A} (set : AVLTree A) : List A :=
+  rfor (acc := nil) (x in set) {
+    x :: acc
+  };
 
---- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of both ;AVLTree;s.
+--- 𝒪(n log n). Returns a set containing the elements that are members of `set1` and `set2`.
 {-# specialize: [1] #-}
-intersection {A} {{Ord A}} (tree1 tree2 : AVLTree A) : AVLTree A :=
-  for (acc := empty) (x in tree1)
-    {if
-      | isMember x tree2 := insert x acc
-      | else := acc};
+intersection {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
+  for (acc := empty) (x in set1) {
+    if
+      | isMember x set2 := insert x acc
+      | else := acc
+  };
 
---- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of the first but not the second ;AVLTree;.
+--- 𝒪(n log n). Returns a set containing the elements that are members of `set1` but not of `set2`.
 {-# specialize: [1] #-}
-difference {A} {{Ord A}} (tree1 tree2 : AVLTree A) : AVLTree A :=
-  for (acc := empty) (x in tree1)
-    {if
-      | isMember x tree2 := acc
-      | else := insert x acc};
+difference {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
+  for (acc := empty) (x in set1) {
+    if
+      | isMember x set2 := acc
+      | else := insert x acc
+  };
 
---- 𝒪(n log n). Returns an ;AVLTree; containing elements that are members of either the first or second ;AVLTree;.
+--- 𝒪(n log n). Returns a set containing the elements that are members of `set1` or `set2`.
 {-# specialize: [1] #-}
-union {A} {{Ord A}} (tree1 tree2 : AVLTree A) : AVLTree A :=
-  for (acc := tree1) (x in tree2) {insert x acc};
+union {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
+  for (acc := set1) (x in set2) {
+    insert x acc
+  };
 
 syntax iterator all {init := 0; range := 1};
---- 𝒪(𝓃). Returns ;true; if all elements of the ;AVLTree; satisfy the predicate.
+--- 𝒪(𝓃). Returns ;true; if all elements of `set` satisfy `predicate`.
 {-# specialize: [1] #-}
-all {A} (predicate : A -> Bool) (tree : AVLTree A) : Bool :=
+all {A} (predicate : A -> Bool) (set : AVLTree A) : Bool :=
   let
     go : AVLTree A -> Bool
       | empty := true
       | node@{element; left; right} := predicate element && go left && go right;
-  in go tree;
+  in go set;
 
 syntax iterator any {init := 0; range := 1};
---- 𝒪(𝓃). Returns ;true; if some elements of the ;AVLTree; satisfies the predicate.
+--- 𝒪(𝓃). Returns ;true; if some element of `set` satisfies `predicate`.
 {-# specialize: [1] #-}
-any {A} (predicate : A -> Bool) (tree : AVLTree A) : Bool :=
+any {A} (predicate : A -> Bool) (set : AVLTree A) : Bool :=
   let
     go : AVLTree A -> Bool
       | empty := true
       | node@{element; left; right} := predicate element || go left || go right;
-  in go tree;
+  in go set;
 
 syntax iterator filter {init := 0; range := 1};
---- 𝒪(n log n). Returns an ;AVLTree; containing all elements of the tree that satisfy the predicate.
+--- 𝒪(n log n). Returns a set containing all elements of `set` that satisfy `predicate`.
 {-# specialize: [1] #-}
-filter {A} {{Ord A}} (predicate : A -> Bool) (tree : AVLTree A) : AVLTree A :=
-  for (acc := empty) (x in tree)
-    {if
+filter {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : AVLTree A :=
+  for (acc := empty) (x in set) {
+    if
       | predicate x := insert x acc
-      | else := acc};
+      | else := acc
+  };
 
 syntax iterator partition {init := 0; range := 1};
-partition {A} {{Ord A}} (predicate : A -> Bool) (tree : AVLTree A) : Pair (AVLTree A) (AVLTree A) :=
-  for (trueSet, falseSet := empty, empty) (x in tree)
-    {if
+partition {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : Pair (AVLTree A) (AVLTree A) :=
+  for (trueSet, falseSet := empty, empty) (x in set) {
+    if
       | predicate x := insert x trueSet, falseSet
-      | else := trueSet, insert x falseSet};
+      | else := trueSet, insert x falseSet
+  };
 
---- 𝒪(1). Creates an ;AVLTree; with a single element.
-singleton {A} (element : A) : AVLTree A := mkNode element empty empty;
+--- 𝒪(1). Creates a set with a single element `elem`.
+singleton {A} (elem : A) : AVLTree A := mkNode elem empty empty;
 
---- 𝒪(n log n). Checks if all elements of tree1 are in tree2.
-isSubset {A} {{Ord A}} (tree1 tree2 : AVLTree A) : Bool := all (x in tree1) {isMember x tree2};
+--- 𝒪(n log n). Checks if all elements of `set1` are in `set2`.
+isSubset {A} {{Ord A}} (set1 set2 : AVLTree A) : Bool :=
+  all (x in set1) {
+    isMember x set2
+  };
 
 syntax iterator map {init := 0; range := 1};
-map {A B} {{Ord B}} (f : A -> B) (tree : AVLTree A) : AVLTree B :=
-  for (acc := empty) (x in tree) {insert (f x) acc};
+map {A B} {{Ord B}} (fun : A -> B) (set : AVLTree A) : AVLTree B :=
+  for (acc := empty) (x in set) {
+    insert (fun x) acc
+  };
 
---- Formats the tree in a debug friendly format.
-prettyDebug {A} {{Show A}} (tree : AVLTree A) : String :=
+--- Formats the set in a debug friendly format.
+prettyDebug {A} {{Show A}} (set : AVLTree A) : String :=
   let
     go : AVLTree A -> String
       | empty := "_"
-      | tree@node@{element; left; right} :=
+      | set@node@{element; left; right} :=
         "("
           ++str go left
           ++str " h"
-          ++str Show.show (diffFactor tree)
+          ++str Show.show (diffFactor set)
           ++str " "
           ++str Show.show element
           ++str " "
           ++str go right
           ++str ")";
-  in go tree;
+  in go set;
 
 --- 𝒪(𝓃).
-toTree {A} : (tree : AVLTree A) -> Maybe (Tree A)
+toTree {A} : (set : AVLTree A) -> Maybe (Tree A)
   | empty := nothing
   | 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}} (tree : AVLTree A) : String := maybe "empty" Tree.treeToString (toTree tree);
+pretty {A} {{Show A}} (set : AVLTree A) : String := maybe "empty" Tree.treeToString (toTree set);
 
 instance
 eqAVLTreeI {A} {{Eq A}} : Eq (AVLTree A) := mkEq (Eq.eq on toList);
diff --git a/Stdlib/Data/UnbalancedSet.juvix b/Stdlib/Data/UnbalancedSet.juvix
index d95c759f..1f0b5dc4 100644
--- a/Stdlib/Data/UnbalancedSet.juvix
+++ b/Stdlib/Data/UnbalancedSet.juvix
@@ -46,7 +46,7 @@ length {A} (set : UnbalancedSet A) : Nat := Tree.length (UnbalancedSet.tree set)
 toList {A} (set : UnbalancedSet A) : List A := Tree.toList (UnbalancedSet.tree set);
 
 instance
-unbalancedSetOrdI {A} {{Ord A}} : Ord (UnbalancedSet A) :=
+ordUnbalancedSetI {A} {{Ord A}} : Ord (UnbalancedSet A) :=
   mkOrd@{
     cmp (s1 s2 : UnbalancedSet A) : Ordering := Ord.cmp (toList s1) (toList s2)
   };
diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix
index c96007f3..ff27d6b2 100644
--- a/Stdlib/Trait/Applicative.juvix
+++ b/Stdlib/Trait/Applicative.juvix
@@ -23,7 +23,7 @@ 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 :=
-  ap (map λ {_ b := b} fa) fb;
+  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 :=
@@ -38,7 +38,10 @@ mapA_
   {{Applicative f}}
   (fun : A -> f B)
   (l : t A)
-  : f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc};
+  : 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)
   | zero _ := pure []
diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
index 329b6472..50b843cd 100644
--- a/Stdlib/Trait/Foldable/Monomorphic.juvix
+++ b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -35,7 +35,10 @@ foldl
   (fun : Acc -> Elem -> Acc)
   (initialValue : Acc)
   (container : Container)
-  : Acc := for (acc := initialValue) (x in container) {fun acc x};
+  : 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 #-}
diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix
index 782d4512..55004fac 100644
--- a/Stdlib/Trait/Foldable/Polymorphic.juvix
+++ b/Stdlib/Trait/Foldable/Polymorphic.juvix
@@ -24,7 +24,10 @@ foldl
   (fun : Acc -> Elem -> Acc)
   (initialValue : Acc)
   (container : F Elem)
-  : Acc := for (acc := initialValue) (x in container) {fun acc x};
+  : 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 #-}
@@ -35,4 +38,7 @@ foldr
   (fun : Elem -> Acc -> Acc)
   (initialValue : Acc)
   (container : F Elem)
-  : Acc := rfor (acc := initialValue) (x in container) {fun x acc};
+  : 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 24ac2c9f..70a641f3 100644
--- a/Stdlib/Trait/Functor/Monomorphic.juvix
+++ b/Stdlib/Trait/Functor/Monomorphic.juvix
@@ -37,4 +37,4 @@ $>
   {{Functor Container Elem}}
   (container : Container)
   (element : Elem)
-  : Container := \ {_ := element} <$> container;
+  : Container := \{_ := element} <$> container;
diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix
index a63ec70c..8a637efc 100644
--- a/Stdlib/Trait/Functor/Polymorphic.juvix
+++ b/Stdlib/Trait/Functor/Polymorphic.juvix
@@ -20,7 +20,7 @@ syntax operator <$> lapp;
 
 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;
diff --git a/test/Test.juvix b/test/Test.juvix
index 1409f631..26084f70 100644
--- a/test/Test.juvix
+++ b/test/Test.juvix
@@ -73,7 +73,7 @@ propZipWith (f : Int -> Int -> Int) (xs ys : List Int) : Bool :=
     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);
+    && eqListInt (map λ{x := f x x} xs) (zipWith f xs xs);
 
 propSnoc (xs : List Int) (x : Int) : Bool :=
   let
@@ -110,7 +110,10 @@ propFoundElementSatisfiesPredicate (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);
+    | nothing :=
+      all (x in xs) {
+        not (p x)
+      };
 
 propFindConsistentWithSplitAt (n : Nat) (p : Int -> Bool) (xs : List Int) : Bool :=
   let
@@ -280,7 +283,7 @@ resultMapOk : QC.Test := QC.mkTest "result: mapOk" propResultMapOk;
 
 main : IO :=
   readLn
-      \ {seed :=
+      \{seed :=
         let
           seedNat := stringToNat seed;
         in QC.runTestsIO
diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix
index 33670451..15b502a0 100644
--- a/test/Test/AVL.juvix
+++ b/test/Test/AVL.juvix
@@ -9,7 +9,7 @@ import Stdlib.Data.Set.AVL as AVL open;
 type Box := mkBox@{b : Nat};
 
 instance
-BoxOrdI : Ord Box := mkOrd (Ord.cmp on Box.b);
+ordBoxI : Ord Box := mkOrd (Ord.cmp on Box.b);
 
 --- Test for size and balance.
 mkTests {A} (descr : TestDescr A) : List Test :=
@@ -21,7 +21,7 @@ mkTests {A} (descr : TestDescr A) : List Test :=
         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))
+         ; testCase (mkTitle "balanced") (assertTrue balanceMsg (Internal.isBalanced testSet))
          ];
 
 type TestDescr (A : Type) :=
@@ -104,10 +104,14 @@ tests : List Test :=
     (assertEqual "map (+ 1) s2" [1; 2; 3; 4; 5; 9] (AVL.map ((+) 1) s2Tree |> AVL.toList))
   ; 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; s2Delete];
 
diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix
index 10c5b0a3..c7a2521b 100644
--- a/test/Test/Arb.juvix
+++ b/test/Test/Arb.juvix
@@ -11,7 +11,7 @@ arbitrarySizedList {A} (size : Nat) (arbitraryA : Arbitrary A) : Arbitrary (List
     mkArbitrary g :=
       mkArbitrary
         (mkGen
-          \ {rand :=
+          \{rand :=
             let
               randList : StdGen -> Nat -> List A
                 | _ zero := nil
@@ -27,7 +27,7 @@ arbitrarySizedList {A} (size : Nat) (arbitraryA : Arbitrary A) : Arbitrary (List
 arbitraryMatrix {A} {{arbA : Arbitrary A}} : Arbitrary (List (List A)) :=
   mkArbitrary
     (mkGen
-      \ {rand :=
+      \{rand :=
         let
           randSplit : Pair StdGen StdGen := stdSplit rand;
           rand1 : StdGen := fst randSplit;
diff --git a/test/Test/Map.juvix b/test/Test/Map.juvix
index 7865afdc..7e83057b 100644
--- a/test/Test/Map.juvix
+++ b/test/Test/Map.juvix
@@ -62,28 +62,28 @@ tests : List Test :=
      ; testCase "Map.isMember" (assertEqual "expected non-member" (Map.isMember 3 m) false)
      ; testCase
        "Map.filter"
-       (assertEqListPair (Map.toList (Map.filter \ {k v := k + v > 3} m2)) [3, 4])
+       (assertEqListPair (Map.toList (Map.filter \{k v := k + v > 3} m2)) [3, 4])
      ; testCase
        "Map.partition"
        (assertEqual
          "expected partition"
          ([1, 2], [3, 4])
-         (Map.partition \ {k v := k < 3} m2 |> both Map.toList))
+         (Map.partition \{k v := k < 3} m2 |> both Map.toList))
      ; testCase
        "Map.mapValuesWithKey"
-       (assertEqListPair (Map.toList (Map.mapValuesWithKey \ {k v := k + v} m2)) [1, 3; 3, 7])
+       (assertEqListPair (Map.toList (Map.mapValuesWithKey \{k v := k + v} m2)) [1, 3; 3, 7])
      ; testCase
        "Map.mapValues"
        (assertEqListPair (Map.toList (Map.mapValues ((+) 1) m2)) [1, 3; 3, 5])
      ; testCase "Map.map" (assertEqListPair (Map.toList (map ((+) 1) m2)) [1, 3; 3, 5])
-     ; testCase "Map.all" (assertTrue "expected all to be true" (Map.all \ {_ v := v > 0} m2))
-     ; testCase "Map.any" (assertTrue "expected any to be true" (Map.any \ {_ v := v > 3} m2))
+     ; testCase "Map.all" (assertTrue "expected all to be true" (Map.all \{_ v := v > 0} m2))
+     ; testCase "Map.any" (assertTrue "expected any to be true" (Map.any \{_ v := v > 3} m2))
      ; testCase
        "Map.foldl"
-       (assertEqual "expected foldl" (Map.foldl \ {acc k v := acc + k + v} 0 m2) 10)
+       (assertEqual "expected foldl" (Map.foldl \{acc k v := acc + k + v} 0 m2) 10)
      ; testCase
        "Map.foldr"
-       (assertEqual "expected foldr" (Map.foldr \ {acc k v := acc + k + v} 0 m2) 10)
+       (assertEqual "expected foldr" (Map.foldr \{acc k v := acc + k + v} 0 m2) 10)
      ; testCase "Map.singleton" (assertEqListPair (Map.toList (Map.singleton 1 2)) [1, 2])
      ];