diff --git a/Stdlib/Cairo/Ec.juvix b/Stdlib/Cairo/Ec.juvix
index a9be50c0..46a4f07e 100644
--- a/Stdlib/Cairo/Ec.juvix
+++ b/Stdlib/Cairo/Ec.juvix
@@ -13,20 +13,24 @@ import Stdlib.Data.Pair open;
 module StarkCurve;
   ALPHA : Field := 1;
 
-  BETA : Field := 0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89;
+  BETA : Field :=
+    0x6f21413efbe40de150e596d72f7a8c5609ad26c15c915c1f4cdfcb99cee9e89;
 
-  ORDER : Field := 0x800000000000010ffffffffffffffffb781126dcae7b2321e66a241adc64d2f;
+  ORDER : Field :=
+    0x800000000000010ffffffffffffffffb781126dcae7b2321e66a241adc64d2f;
 
-  GEN_X : Field := 0x1ef15c18599971b7beced415a40f0c7deacfd9b0d1819e03d723d8bc943cfca;
+  GEN_X : Field :=
+    0x1ef15c18599971b7beced415a40f0c7deacfd9b0d1819e03d723d8bc943cfca;
 
-  GEN_Y : Field := 0x5668060aa49730b7be4801df46ec62de53ecd11abe43a32873000c36e8dc1f;
+  GEN_Y : Field :=
+    0x5668060aa49730b7be4801df46ec62de53ecd11abe43a32873000c36e8dc1f;
 end;
 
 builtin ec_point
 type Point :=
   mkPoint@{
     x : Field;
-    y : Field
+    y : Field;
   };
 
 module Internal;
@@ -57,9 +61,9 @@ double (point : Point) : Point :=
             r_x := slope * slope - x - x;
             r_y := slope * (x - r_x) - y;
           in mkPoint@?{
-            x := r_x;
-            y := r_y
-          };
+               x := r_x;
+               y := r_y;
+             };
 
 --- Adds two valid points on the EC.
 add (point1 point2 : Point) : Point :=
diff --git a/Stdlib/Cairo/Poseidon.juvix b/Stdlib/Cairo/Poseidon.juvix
index 2e19df00..c205803c 100644
--- a/Stdlib/Cairo/Poseidon.juvix
+++ b/Stdlib/Cairo/Poseidon.juvix
@@ -8,7 +8,7 @@ type PoseidonState :=
   mkPoseidonState@{
     s0 : Field;
     s1 : Field;
-    s2 : Field
+    s2 : Field;
   };
 
 builtin poseidon
@@ -19,11 +19,13 @@ axiom poseidonHash : PoseidonState -> PoseidonState;
 
 --- Hashes one element and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHash1 (x : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseidonState x 0 1));
+poseidonHash1 (x : Field) : Field :=
+  PoseidonState.s0 (poseidonHash (mkPoseidonState x 0 1));
 
 --- Hashes two elements and retrieves a single field element output.
 {-# eval: false #-}
-poseidonHash2 (x y : Field) : Field := PoseidonState.s0 (poseidonHash (mkPoseidonState x y 2));
+poseidonHash2 (x y : Field) : Field :=
+  PoseidonState.s0 (poseidonHash (mkPoseidonState x y 2));
 
 --- Hashes n elements and retrieves a single field element output.
 {-# eval: false #-}
@@ -31,7 +33,7 @@ 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 }
+      | [x] := poseidonHash acc@PoseidonState{s0 := s0 + x; s1 := s1 + 1}
       | (x1 :: x2 :: xs) :=
-        go (poseidonHash acc@PoseidonState{   s0 := s0 + x1; s1 := s1 + x2 }) xs;
+        go (poseidonHash acc@PoseidonState{s0 := s0 + x1; s1 := s1 + x2}) xs;
   in PoseidonState.s0 (go (mkPoseidonState 0 0 0) list);
diff --git a/Stdlib/Data/BinaryTree.juvix b/Stdlib/Data/BinaryTree.juvix
index 4da9aab2..78462681 100644
--- a/Stdlib/Data/BinaryTree.juvix
+++ b/Stdlib/Data/BinaryTree.juvix
@@ -8,7 +8,7 @@ type BinaryTree (A : Type) :=
   | node@{
       left : BinaryTree A;
       element : A;
-      right : BinaryTree A
+      right : BinaryTree A;
     };
 
 --- fold a tree in depth-first order
@@ -21,4 +21,5 @@ fold {A B} (f : A -> B -> B -> B) (acc : B) (tree : BinaryTree A) : B :=
 
 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 50423dc5..73490d07 100644
--- a/Stdlib/Data/Bool.juvix
+++ b/Stdlib/Data/Bool.juvix
@@ -15,7 +15,7 @@ eqBoolI : Eq Bool :=
       case x, y of
         | true, true := true
         | false, false := true
-        | _ := false
+        | _ := false;
   };
 
 {-# specialize: true, inline: case #-}
@@ -27,7 +27,7 @@ ordBoolI : Ord Bool :=
         | false, false := Equal
         | false, true := LessThan
         | true, false := GreaterThan
-        | true, true := Equal
+        | true, true := Equal;
   };
 
 instance
@@ -36,5 +36,5 @@ showBoolI : Show Bool :=
     show (x : Bool) : String :=
       if
         | x := "true"
-        | else := "false"
+        | else := "false";
   };
diff --git a/Stdlib/Data/Byte.juvix b/Stdlib/Data/Byte.juvix
index 99bb444c..72fc1000 100644
--- a/Stdlib/Data/Byte.juvix
+++ b/Stdlib/Data/Byte.juvix
@@ -17,12 +17,12 @@ eqByteI : Eq Byte := mkEq (Byte.==);
 instance
 showByteI : Show Byte :=
   mkShow@{
-    show (x : Byte) : String := Show.show (Byte.toNat x)
+    show (x : Byte) : String := Show.show (Byte.toNat x);
   };
 
 {-# specialize: true, inline: case #-}
 instance
 fromNaturalByteI : FromNatural Byte :=
   mkFromNatural@{
-    fromNat := Byte.fromNat
+    fromNat := Byte.fromNat;
   };
diff --git a/Stdlib/Data/Field.juvix b/Stdlib/Data/Field.juvix
index 7362a7df..b11c5fae 100644
--- a/Stdlib/Data/Field.juvix
+++ b/Stdlib/Data/Field.juvix
@@ -19,14 +19,14 @@ eqFieldI : Eq Field := mkEq (Field.==);
 instance
 showFieldI : Show Field :=
   mkShow@{
-    show (f : Field) : String := Show.show (Field.toNat f)
+    show (f : Field) : String := Show.show (Field.toNat f);
   };
 
 {-# specialize: true, inline: case #-}
 instance
 fromNaturalFieldI : FromNatural Field :=
   mkFromNatural@{
-    fromNat := Field.fromNat
+    fromNat := Field.fromNat;
   };
 
 {-# specialize: true, inline: case #-}
@@ -34,7 +34,7 @@ instance
 naturalFieldI : Natural Field :=
   mkNatural@{
     + := (Field.+);
-    * := (Field.*)
+    * := (Field.*);
   };
 
 {-# specialize: true, inline: case #-}
@@ -43,7 +43,7 @@ integralFieldI : Integral Field :=
   mkIntegral@{
     naturalI := naturalFieldI;
     - := (Field.-);
-    fromInt := Field.fromInt
+    fromInt := Field.fromInt;
   };
 
 {-# specialize: true, inline: case #-}
@@ -51,5 +51,5 @@ instance
 numericFieldI : Numeric Field :=
   mkNumeric@{
     integralI := integralFieldI;
-    / := (Field./)
+    / := (Field./);
   };
diff --git a/Stdlib/Data/Int.juvix b/Stdlib/Data/Int.juvix
index d9968c3f..cf62bf77 100644
--- a/Stdlib/Data/Int.juvix
+++ b/Stdlib/Data/Int.juvix
@@ -37,7 +37,7 @@ showIntI : Show Int := mkShow intToString;
 instance
 fromNaturalIntI : FromNatural Int :=
   mkFromNatural@{
-    fromNat := ofNat
+    fromNat := ofNat;
   };
 
 {-# specialize: true, inline: case #-}
@@ -45,7 +45,7 @@ instance
 naturalIntI : Natural Int :=
   mkNatural@{
     + := (Int.+);
-    * := (Int.*)
+    * := (Int.*);
   };
 
 {-# specialize: true, inline: case #-}
@@ -54,7 +54,7 @@ integralIntI : Integral Int :=
   mkIntegral@{
     naturalI := naturalIntI;
     - := (Int.-);
-    fromInt (x : Int) : Int := x
+    fromInt (x : Int) : Int := x;
   };
 
 {-# specialize: true, inline: case #-}
@@ -62,5 +62,5 @@ instance
 divModIntI : DivMod Int :=
   mkDivMod@{
     div := Int.div;
-    mod := Int.mod
+    mod := Int.mod;
   };
diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
index 31de9aa8..f62aa06d 100644
--- a/Stdlib/Data/List.juvix
+++ b/Stdlib/Data/List.juvix
@@ -10,7 +10,11 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait open;
 import Stdlib.Trait.Partial open;
-import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable};
+import Stdlib.Trait.Foldable open using {
+  Foldable;
+  module Polymorphic;
+  fromPolymorphicFoldable;
+};
 
 --- 𝒪(1). Partial function that returns the first element of a ;List;.
 phead {A} {{Partial}} : List A -> A
@@ -30,7 +34,8 @@ eqListI {A} {{Eq A}} : Eq (List A) :=
           | else := false;
   in mkEq go;
 
-isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool := isElement (Eq.eq) elem list;
+isMember {A} {{Eq A}} (elem : A) (list : List A) : Bool :=
+  isElement (Eq.eq) elem list;
 
 instance
 ordListI {A} {{Ord A}} : Ord (List A) :=
@@ -53,29 +58,30 @@ showListI {A} {{Show A}} : Show (List A) :=
       | nil := "nil"
       | (x :: xs) := Show.show x ++str " :: " ++str go xs;
   in mkShow@{
-    show (list : List A) : String :=
-      case list of
-        | nil := "nil"
-        | s := "(" ++str go s ++str ")"
-  };
+       show (list : List A) : String :=
+         case list of
+           | nil := "nil"
+           | s := "(" ++str go s ++str ")";
+     };
 
 {-# specialize: true, inline: case #-}
 instance
 functorListI : Functor List :=
   mkFunctor@{
-    map := listMap
+    map := listMap;
   };
 
 {-# specialize: true, inline: true #-}
 instance
-monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A := fromPolymorphicFunctor;
+monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A :=
+  fromPolymorphicFunctor;
 
 {-# specialize: true, inline: case #-}
 instance
 polymorphicFoldableListI : Polymorphic.Foldable List :=
   Polymorphic.mkFoldable@{
     for := listFor;
-    rfor := listRfor
+    rfor := listRfor;
   };
 
 {-# specialize: true, inline: true #-}
@@ -88,11 +94,11 @@ applicativeListI : Applicative List :=
     pure {A} (a : A) : List A := [a];
     ap {A B} : (listOfFuns : List (A -> B)) -> (listOfAs : List A) -> List B
       | [] _ := []
-      | (f :: fs) l := map f l ++ ap fs l
+      | (f :: fs) l := map f l ++ ap fs l;
   };
 
 instance
 monadListI : Monad List :=
   mkMonad@{
-    bind := flip concatMap
+    bind := flip concatMap;
   };
diff --git a/Stdlib/Data/List/Base.juvix b/Stdlib/Data/List/Base.juvix
index 99f880dc..bc8d0900 100644
--- a/Stdlib/Data/List/Base.juvix
+++ b/Stdlib/Data/List/Base.juvix
@@ -34,7 +34,8 @@ listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> B
 
 --- Right-associative fold.
 {-# specialize: [1] #-}
-liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : B := listRfor (flip fun) acc list;
+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] #-}
@@ -138,7 +139,8 @@ snoc {A} (list : List A) (elem : A) : List A := list ++ elem :: nil;
 
 --- Concatenates a ;List; of ;List;s.
 {-# isabelle-function: {name: "concat"} #-}
-flatten {A} (listOfLists : List (List A)) : List A := listFoldl (++) nil listOfLists;
+flatten {A} (listOfLists : List (List A)) : List A :=
+  listFoldl (++) nil listOfLists;
 
 --- 𝒪(𝓃). Inserts the given separator before every element in the given ;List;.
 prependToAll {A} (separator : A) : (list : List A) -> List A
@@ -194,7 +196,8 @@ 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) : (list1 : List A) -> (list2 : 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;
@@ -231,7 +234,8 @@ 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;.
@@ -244,7 +248,8 @@ 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} (fun : A -> List B) (list : List A) : List B := flatten (listMap fun list);
+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} : (listOfLists : List (List A)) -> List (List A)
diff --git a/Stdlib/Data/Map.juvix b/Stdlib/Data/Map.juvix
index 63c89171..75ee1f53 100644
--- a/Stdlib/Data/Map.juvix
+++ b/Stdlib/Data/Map.juvix
@@ -2,6 +2,7 @@ module Stdlib.Data.Map;
 
 import Stdlib.Data.Pair open;
 import Stdlib.Data.Maybe open;
+import Stdlib.Data.Result open;
 import Stdlib.Data.List open;
 import Stdlib.Data.Nat open;
 import Stdlib.Data.Bool open;
@@ -20,27 +21,29 @@ import Stdlib.Data.BinaryTree as Tree;
 type Binding Key Value :=
   mkBinding@{
     key : Key;
-    value : Value
+    value : Value;
   };
 
 key {Key Value} (binding : Binding Key Value) : Key := Binding.key binding;
 
-value {Key Value} (binding : Binding Key Value) : Value := Binding.value binding;
+value {Key Value} (binding : Binding Key Value) : Value :=
+  Binding.value binding;
 
-toPair {Key Value} (binding : Binding Key Value) : Pair Key Value := key binding, value binding;
+toPair {Key Value} (binding : Binding Key Value) : Pair Key Value :=
+  key binding, value binding;
 
 instance
 bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) :=
   mkOrd@{
     {-# inline: true #-}
-    cmp (b1 b2 : Binding Key Value) : Ordering := Ord.cmp (key b1) (key b2)
+    cmp (b1 b2 : Binding Key Value) : Ordering := Ord.cmp (key b1) (key b2);
   };
 
 type Map Key Value := mkMap (AVLTree (Binding Key Value));
 
 empty {Key Value} : Map Key Value := mkMap AVL.empty;
 
-{-# specialize: [1, f] #-}
+{-# specialize: [1, fun] #-}
 insertWith
   {Key Value}
   {{Ord Key}}
@@ -53,7 +56,8 @@ insertWith
     mkMap tree :=
       let
         fun' (binding1 binding2 : Binding Key Value) : Binding Key Value :=
-          case binding1, binding2 of mkBinding k b1, mkBinding _ b2 := mkBinding k (fun b1 b2);
+          case binding1, binding2 of
+            mkBinding k b1, mkBinding _ b2 := mkBinding k (fun b1 b2);
         binding := mkBinding key value;
       in mkMap (Set.insertWith fun' binding tree);
 
@@ -62,12 +66,17 @@ insertWith
 --- `value`.
 {-# inline: true #-}
 insert
-  {Key Value : Type} {{Ord Key}} (key : Key) (elem : Value) (map : Map Key Value) : Map Key Value :=
-  insertWith (flip const) key elem map;
+  {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 `map`.
 {-# specialize: [1] #-}
-lookup {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Maybe Value :=
+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 `map`.
@@ -75,7 +84,7 @@ lookup {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Maybe Value :
 isMember {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Bool :=
   isJust (lookup key map);
 
-{-# specialize: [1, f] #-}
+{-# specialize: [1, fun] #-}
 fromListWithKey
   {Key Value}
   {{Ord Key}}
@@ -95,7 +104,8 @@ fromListWith
   : Map Key Value := fromListWithKey (const fun) list;
 
 {-# inline: true #-}
-fromList {Key Value} {{Ord Key}} (list : List (Pair Key Value)) : Map Key Value :=
+fromList
+  {Key Value} {{Ord Key}} (list : List (Pair Key Value)) : Map Key Value :=
   fromListWith (flip const) list;
 
 toList {Key Value} (map : Map Key Value) : List (Pair Key Value) :=
@@ -105,23 +115,50 @@ toList {Key Value} (map : Map Key Value) : List (Pair Key Value) :=
         toPair x
       };
 
-{-# specialize: [1, f] #-}
-fromSet {Key Value} {{Ord Key}} (fun : Key -> Value) (set : Set Key) : Map Key Value :=
+{-# specialize: [1, fun] #-}
+fromSetWithFun
+  {Key Value}
+  {{Ord Key}}
+  (fun : Key -> Value)
+  (set : Set Key)
+  : Map Key Value :=
   for (acc := empty) (k in set) {
     insert k (fun k) acc
   };
 
+{-# specialize: [1] #-}
+fromSet {Key Value} {{Ord Key}} (set : Set (Pair Key Value)) : Map Key Value :=
+  for (acc := empty) (k, v in set) {
+    insert k v acc
+  };
+
+{-# specialize: [1, 2] #-}
+toSet
+  {Key Value}
+  {{Ord Key}}
+  {{Ord Value}}
+  (map : Map Key Value)
+  : Set (Pair Key Value) :=
+  case map of
+    mkMap s :=
+      Set.map (x in s) {
+        toPair x
+      };
+
 --- 𝒪(1). Checks if a ;Map; is empty.
 {-# inline: true #-}
-isEmpty {Key Value} (map : Map Key Value) : Bool := case map 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} (map : Map Key Value) : Nat := case map of mkMap s := Set.size s;
+size {Key Value} (map : Map Key Value) : Nat :=
+  case map of mkMap s := Set.size s;
 
 --- 𝒪(log 𝓃). Removes `key` assignment from `map`.
 {-# inline: true #-}
-delete {Key Value} {{Ord Key}} (key : Key) (map : Map Key Value) : Map Key Value :=
+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} (map : Map Key Value) : List Key :=
@@ -152,22 +189,35 @@ valueSet {Key Value} {{Ord Value}} (map : Map Key Value) : Set Value :=
         value x
       };
 
-{-# specialize: [f] #-}
+{-# specialize: [fun] #-}
 mapValuesWithKey
-  {Key Value1 Value2} (fun : Key -> Value1 -> Value2) (map : Map Key Value1) : Map Key Value2 :=
+  {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);
+    mkMap s :=
+      mkMap
+        (Set.Internal.unsafeMap \{(mkBinding k v) := mkBinding k (fun k v)} s);
 
 {-# inline: true #-}
-mapValues {Key Value1 Value2} (fun : Value1 -> Value2) (map : Map Key Value1) : Map Key Value2 :=
-  mapValuesWithKey (const fun) map;
+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} (fun : Key -> Value -> Acc -> Acc) (acc : Acc) (map : Map Key Value) : 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) {
@@ -175,17 +225,75 @@ foldr {Key Value Acc} (fun : Key -> Value -> Acc -> Acc) (acc : Acc) (map : Map
       };
 
 {-# inline: true #-}
-foldl {Key Value Acc} (fun : Acc -> Key -> Value -> Acc) (acc : Acc) (map : Map Key Value) : Acc :=
+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)
       };
 
+--- 𝒪(n log n). Intersection of two maps. Returns data in the first map for the
+--- keys existing in both maps.
+{-# inline: true #-}
+intersection
+  {Key Value} {{Ord Key}} (map1 map2 : Map Key Value) : Map Key Value :=
+  case map1, map2 of mkMap s1, mkMap s2 := mkMap (Set.intersection s1 s2);
+
+--- 𝒪(n log n). Return elements of `map1` with keys not existing in `map2`.
+{-# inline: true #-}
+difference
+  {Key Value} {{Ord Key}} (map1 map2 : Map Key Value) : Map Key Value :=
+  case map1, map2 of mkMap s1, mkMap s2 := mkMap (Set.difference s1 s2);
+
+--- 𝒪(n log n). Returns a ;Map; containing the elements that are in `map1` or
+--- `map2`. This is a left-biased union of `map1` and `map2` which prefers
+--- `map1` when duplicate keys are encountered.
+{-# inline: true #-}
+unionLeft {Key Value} {{Ord Key}} (map1 map2 : Map Key Value) : Map Key Value :=
+  case map1, map2 of mkMap s1, mkMap s2 := mkMap (Set.unionLeft s1 s2);
+
+--- 𝒪(n log n). Returns a ;Map; containing the elements that are in `map1` or `map2`.
+{-# inline: true #-}
+union {Key Value} {{Ord Key}} (map1 map2 : Map Key Value) : Map Key Value :=
+  case map1, map2 of mkMap s1, mkMap s2 := mkMap (Set.union s1 s2);
+
+{-# specialize: [1, 2] #-}
+unions
+  {Key Value Container}
+  {{Ord Key}}
+  {{Foldable Container (Map Key Value)}}
+  (maps : Container)
+  : Map Key Value :=
+  for (acc := empty) (map in maps) {
+    union acc map
+  };
+
+--- O(n log n). If `map1` and `map2` are disjoint (have no common keys), then
+--- returns `ok map` where `map` is the union of `map1` and `map2`. If `map1`
+--- and `map2` are not disjoint, then returns `error k` where `k` is a common
+--- key.
+{-# inline: true #-}
+disjointUnion
+  {Key Value}
+  {{Ord Key}}
+  (map1 map2 : Map Key Value)
+  : Result Key (Map Key Value) :=
+  case map1, map2 of
+    mkMap s1, mkMap s2 :=
+      case Set.disjointUnion s1 s2 of
+        | error x := error (key x)
+        | ok s := ok (mkMap s);
+
 syntax iterator all {init := 0; range := 1};
 --- 𝒪(𝓃). Returns ;true; if all key-value pairs in `map` satisfy `predicate`.
 {-# inline: true #-}
-all {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
+all
+  {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
   case map of
     mkMap s :=
       Set.all (x in s) {
@@ -195,7 +303,8 @@ all {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool
 syntax iterator any {init := 0; range := 1};
 --- 𝒪(𝓃). Returns ;true; if some key-value pair in `map` satisfies `predicate`.
 {-# inline: true #-}
-any {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
+any
+  {Key Value} (predicate : Key -> Value -> Bool) (map : Map Key Value) : Bool :=
   case map of
     mkMap s :=
       Set.any (x in s) {
@@ -239,7 +348,8 @@ partition
 instance
 functorMapI {Key} : Functor (Map Key) :=
   mkFunctor@{
-    map {A B} (fun : A -> B) (container : Map Key A) : Map Key B := mapValues fun container
+    map {A B} (fun : A -> B) (container : Map Key A) : Map Key B :=
+      mapValues fun container;
   };
 
 {-# specialize: true, inline: case #-}
@@ -247,12 +357,14 @@ instance
 foldableMapI {Key Value} : Foldable (Map Key Value) (Pair Key Value) :=
   mkFoldable@{
     {-# inline: true #-}
-    for {B} (f : B -> Pair Key Value -> B) (acc : B) (map : Map Key Value) : B :=
+    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) (map : Map Key Value) : B :=
-      foldr \{k v a := f a (k, v)} acc map
+    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/Maybe.juvix b/Stdlib/Data/Maybe.juvix
index d02e565f..2fff90d6 100644
--- a/Stdlib/Data/Maybe.juvix
+++ b/Stdlib/Data/Maybe.juvix
@@ -21,7 +21,7 @@ eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
       case m1, m2 of
         | nothing, nothing := true
         | just a1, just a2 := Eq.eq a1 a2
-        | _ := false
+        | _ := false;
   };
 
 instance
@@ -30,7 +30,7 @@ showMaybeI {A} {{Show A}} : Show (Maybe A) :=
     show (m : Maybe A) : String :=
       case m of
         | nothing := "nothing"
-        | just a := "just " ++str Show.show a
+        | just a := "just " ++str Show.show a;
   };
 
 {-# specialize: true, inline: case #-}
@@ -42,7 +42,7 @@ ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
         | nothing, nothing := Equal
         | just a1, just a2 := Ord.cmp a1 a2
         | nothing, just _ := LessThan
-        | just _, nothing := GreaterThan
+        | just _, nothing := GreaterThan;
   };
 
 {-# specialize: true, inline: case #-}
@@ -51,12 +51,13 @@ functorMaybeI : Functor Maybe :=
   mkFunctor@{
     map {A B} (f : A -> B) : Maybe A -> Maybe B
       | nothing := nothing
-      | (just a) := just (f a)
+      | (just a) := just (f a);
   };
 
 {-# specizalize: true, inline: true #-}
 instance
-monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;
+monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A :=
+  fromPolymorphicFunctor;
 
 instance
 applicativeMaybeI : Applicative Maybe :=
@@ -65,7 +66,7 @@ applicativeMaybeI : Applicative Maybe :=
     ap {A B} (listOfFuns : Maybe (A -> B)) (list : Maybe A) : Maybe B :=
       case listOfFuns, list of
         | just f, just x := just (f x)
-        | _, _ := nothing
+        | _, _ := nothing;
   };
 
 instance
@@ -74,5 +75,5 @@ monadMaybeI : Monad Maybe :=
     bind {A B} (maybe : Maybe A) (fun : A -> Maybe B) : Maybe B :=
       case maybe of
         | nothing := nothing
-        | just a := fun a
+        | just a := fun a;
   };
diff --git a/Stdlib/Data/Nat.juvix b/Stdlib/Data/Nat.juvix
index ee5ebcee..81d45d07 100644
--- a/Stdlib/Data/Nat.juvix
+++ b/Stdlib/Data/Nat.juvix
@@ -40,5 +40,5 @@ instance
 divModNatI : DivMod Nat :=
   mkDivMod@{
     div := Nat.div;
-    mod := Nat.mod
+    mod := Nat.mod;
   };
diff --git a/Stdlib/Data/Pair.juvix b/Stdlib/Data/Pair.juvix
index feb2a550..bcadcc76 100644
--- a/Stdlib/Data/Pair.juvix
+++ b/Stdlib/Data/Pair.juvix
@@ -13,7 +13,8 @@ instance
 eqProductI {A B} : {{Eq A}} -> {{Eq B}} -> Eq (Pair A B)
   | {{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
+      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 #-}
@@ -27,7 +28,7 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (Pair A B)
             case cmpA a1 a2 of
               | LessThan := LessThan
               | GreaterThan := GreaterThan
-              | Equal := cmpB b1 b2
+              | Equal := cmpB b1 b2;
     };
 
 instance
@@ -35,5 +36,5 @@ showProductI {A B} : {{Show A}} -> {{Show B}} -> Show (Pair A B)
   | {{mkShow showA}} {{mkShow showB}} :=
     mkShow@{
       show (p : Pair A B) : String :=
-        case p of a, b := "(" ++str showA a ++str " , " ++str showB b ++str ")"
+        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 dae78ccc..ea22efcc 100644
--- a/Stdlib/Data/Pair/Base.juvix
+++ b/Stdlib/Data/Pair/Base.juvix
@@ -9,7 +9,8 @@ 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} (fun : A -> B -> C) (pair : Pair A B) : C := case pair of a, b := fun 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} (fun : Pair A B -> C) (a : A) (b : B) : C := fun (a, b);
@@ -24,10 +25,13 @@ 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'} (fun : A -> A') (pair : Pair A B) : Pair A' B := case pair of a, b := fun 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'} (fun : B -> B') (pair : Pair A B) : Pair A B' := case pair of a, b := a, fun 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} (fun : A -> B) (pair : Pair A A) : Pair B B := case pair of a, b := fun a, fun 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 54271825..ba9ee0b7 100644
--- a/Stdlib/Data/Queue/Base.juvix
+++ b/Stdlib/Data/Queue/Base.juvix
@@ -21,7 +21,7 @@ import Stdlib.Trait.Foldable open;
 type Queue (A : Type) :=
   mkQueue@{
     front : List A;
-    back : List A
+    back : List A;
   };
 
 --- 𝒪(1). The empty ;Queue;.
@@ -76,10 +76,12 @@ 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 : Queue A) : List A := case queue of mkQueue 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 : Queue A) : Nat := case queue of mkQueue 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 b825ecbd..8047adee 100644
--- a/Stdlib/Data/Range.juvix
+++ b/Stdlib/Data/Range.juvix
@@ -12,13 +12,13 @@ import Stdlib.Data.Nat open;
 type Range N :=
   mkRange@{
     low : N;
-    high : N
+    high : N;
   };
 
 type StepRange N :=
   mkStepRange@{
     range : Range N;
-    step : N
+    step : N;
   };
 
 syntax operator to range;
@@ -59,7 +59,7 @@ foldableRangeI {N} {{Eq N}} {{Natural N}} : Foldable (Range N) N :=
             if
               | next == high := fun initialValue next
               | else := fun (go (next + 1)) next;
-        in go low
+        in go low;
   };
 
 -- This instance assumes that (low + step*k > high) for some k.
@@ -88,5 +88,5 @@ foldableStepRangeI {N} {{Ord N}} {{Natural N}} : Foldable (StepRange N) N :=
             if
               | next <= high := fun (go (next + step)) next
               | else := initialValue;
-        in go low
+        in go low;
   };
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
index 59430367..8da00279 100644
--- a/Stdlib/Data/Result.juvix
+++ b/Stdlib/Data/Result.juvix
@@ -12,14 +12,15 @@ import Stdlib.Trait open;
 
 {-# specialize: true, inline: case #-}
 instance
-ordResultI {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) :=
+ordResultI
+  {Error Value} {{Ord Error}} {{Ord Value}} : Ord (Result Error Value) :=
   mkOrd@{
     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
+        | ok _, error _ := GreaterThan;
   };
 
 {-# specialize: true, inline: case #-}
@@ -30,45 +31,55 @@ eqResultI {Error Value} {{Eq Error}} {{Eq Value}} : Eq (Result Error Value) :=
       case result1, result2 of
         | error a1, error a2 := a1 == a2
         | ok b1, ok b2 := b1 == b2
-        | _, _ := false
+        | _, _ := false;
   };
 
 instance
-showResultI {Error Value} {{Show Error}} {{Show Value}} : Show (Result Error Value) :=
+showResultI
+  {Error Value} {{Show Error}} {{Show Value}} : Show (Result Error Value) :=
   mkShow@{
     show : Result Error Value -> String
       | (error x) := "Error (" ++str Show.show x ++str ")"
-      | (ok x) := "Ok (" ++str Show.show x ++str ")"
+      | (ok x) := "Ok (" ++str Show.show x ++str ")";
   };
 
 {-# specialize: true, inline: case #-}
 instance
 functorResultI {Error} : Functor (Result Error) :=
   mkFunctor@{
-    map := mapOk
+    map := mapOk;
   };
 
 {-# specialize: true, inline: true #-}
 instance
-monomorphicFunctorResultI {Error Value} : Monomorphic.Functor (Result Error Value) Value :=
+monomorphicFunctorResultI
+  {Error Value} : Monomorphic.Functor (Result Error Value) Value :=
   fromPolymorphicFunctor;
 
 instance
 applicativeResultI {Error} : Applicative (Result Error) :=
   mkApplicative@{
     pure := ok;
-    ap {A B} (resultFun : Result Error (A -> B)) (result : Result Error A) : Result Error B :=
+    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
+        | error e, _ := error e;
   };
 
 instance
 monadResultI {Error} : Monad (Result Error) :=
   mkMonad@{
-    bind {A B} (result : Result Error A) (fun : A -> Result Error B) : Result Error B :=
+    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
+        | ok a := fun a;
   };
diff --git a/Stdlib/Data/Result/Base.juvix b/Stdlib/Data/Result/Base.juvix
index d3ba7865..46c0c601 100644
--- a/Stdlib/Data/Result/Base.juvix
+++ b/Stdlib/Data/Result/Base.juvix
@@ -50,13 +50,15 @@ isOk {Error Value} (result : Result Error Value) : Bool :=
     | ok _ := true;
 
 --- Return the contents of an ;error; value, otherwise return defaultError.
-fromError {Error Value} (defaultError : Error) (result : Result Error Value) : Error :=
+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 defaultValue.
-fromOk {Error Value} (defaultValue : Value) (result : Result Error Value) : Value :=
+fromOk
+  {Error Value} (defaultValue : Value) (result : Result Error Value) : Value :=
   case result of
     | error _ := defaultValue
     | ok b := b;
@@ -67,7 +69,10 @@ resultToMaybe {Error Value} (result : Result Error Value) : Maybe Value :=
 
 --- Convert a Maybe to a Result. A ;nothing; value becomes `error defaultError`.
 maybeToResult
-  {Error Value} (defaultError : Error) (maybeValue : Maybe Value) : Result Error Value :=
+  {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 d66d140d..2a5e6ee1 100644
--- a/Stdlib/Data/Set/AVL.juvix
+++ b/Stdlib/Data/Set/AVL.juvix
@@ -10,6 +10,7 @@ module Stdlib.Data.Set.AVL;
 
 import Stdlib.Data.Tree as Tree open using {Tree; Forest};
 import Stdlib.Data.Maybe open;
+import Stdlib.Data.Result open;
 import Stdlib.Data.Nat open;
 import Stdlib.Data.Int open;
 import Stdlib.Data.Bool open;
@@ -28,7 +29,7 @@ type AVLTree (A : Type) :=
       element : A;
       height : Nat;
       left : AVLTree A;
-      right : AVLTree A
+      right : AVLTree A;
     };
 
 module Internal;
@@ -117,7 +118,8 @@ module Internal;
             }
           | LeanLeft :=
             case balanceFactor left of {
-              | LeanRight := rotateRight (mkNode element (rotateLeft left) right)
+              | LeanRight :=
+                rotateRight (mkNode element (rotateLeft left) right)
               | _ := rotateRight set
             }
           | LeanNone := set;
@@ -126,7 +128,8 @@ module Internal;
   --- 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;
+    | set@node@{left; right} :=
+      isBalanced left && isBalanced right && abs (diffFactor set) <= 1;
 end;
 
 open Internal;
@@ -134,7 +137,13 @@ open Internal;
 --- 𝒪(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) (set : 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
@@ -148,11 +157,13 @@ lookupWith {A K} {{order : Ord K}} (fun : A -> K) (elem : K) (set : AVLTree A) :
 
 --- 𝒪(log 𝓃). Queries whether `elem` is in `set`.
 {-# specialize: [1] #-}
-lookup {A} {{Ord A}} (elem : A) (set : AVLTree A) : Maybe A := lookupWith id elem set;
+lookup {A} {{Ord A}} (elem : A) (set : AVLTree A) : Maybe A :=
+  lookupWith id elem set;
 
 --- 𝒪(log 𝓃). Queries whether `elem` is in `set`.
 {-# specialize: [1] #-}
-isMember {A} {{Ord A}} (elem : A) (set : AVLTree A) : Bool := isJust (lookupWith id elem set);
+isMember {A} {{Ord A}} (elem : A) (set : AVLTree A) : Bool :=
+  isJust (lookupWith id elem set);
 
 --- 𝒪(log 𝓃). Inserts an element `elem` into `set` using a function to
 --- deduplicate entries.
@@ -160,7 +171,13 @@ isMember {A} {{Ord A}} (elem : A) (set : AVLTree A) : Bool := isJust (lookupWith
 --- 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) (set : 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
@@ -174,7 +191,8 @@ insertWith {A} {{order : Ord A}} (fun : A -> A -> A) (elem : A) (set : AVLTree A
 
 --- 𝒪(log 𝓃). Inserts `elem` into `set`.
 {-# specialize: [1] #-}
-insert {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree A := insertWith (flip const) elem set;
+insert {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree A :=
+  insertWith (flip const) elem set;
 
 --- 𝒪(log 𝓃). Removes the minimum element from `set`.
 {-# specialize: [1] #-}
@@ -211,12 +229,14 @@ deleteWith
               | _ :=
                 case deleteMin right of
                   | nothing := left
-                  | just (minRight, right') := balance (mkNode minRight left right');
+                  | just (minRight, right') :=
+                    balance (mkNode minRight left right');
   in go set;
 
 --- 𝒪(log 𝓃). Removes `elem` from `set`.
 {-# specialize: [1] #-}
-delete {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree A := deleteWith id elem set;
+delete {A} {{Ord A}} (elem : A) (set : AVLTree A) : AVLTree A :=
+  deleteWith id elem set;
 
 --- 𝒪(log 𝓃). Returns the minimum element of `set`.
 lookupMin {A} : (set : AVLTree A) -> Maybe A
@@ -242,7 +262,13 @@ deleteMany {A} {{Ord A}} (toDelete : List A) (set : AVLTree A) : AVLTree A :=
 --- 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) (set : AVLTree A) : AVLTree A :=
+  {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
   };
@@ -269,21 +295,25 @@ size {A} : (set : AVLTree A) -> Nat
 {-# specialize: [1] #-}
 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;
+  | node@{element; left; right} :=
+    foldr fun (fun element (foldr fun acc right)) left;
 
 {-# specialize: [1] #-}
 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;
+  | node@{element; left; right} :=
+    foldl fun (fun (foldl fun acc left) element) right;
 
 {-# specialize: true, inline: case #-}
 instance
 polymorphicFoldableAVLTreeI : Polymorphic.Foldable AVLTree :=
   Polymorphic.mkFoldable@{
     {-# inline: true #-}
-    for {A B} (f : B -> A -> B) (acc : B) (set : AVLTree A) : B := foldl f acc set;
+    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) (set : AVLTree A) : B := foldr (flip f) acc set
+    rfor {A B} (f : B -> A -> B) (acc : B) (set : AVLTree A) : B :=
+      foldr (flip f) acc set;
   };
 
 {-# specialize: true, inline: true #-}
@@ -314,13 +344,53 @@ difference {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
       | else := insert x acc
   };
 
---- 𝒪(n log n). Returns a set containing the elements that are members of `set1` or `set2`.
+--- 𝒪(n log (m + n)). Returns a set containing the elements that are members of
+--- `set1` or `set2`. This is a left-biased union of `set1` and `set2` which
+--- prefers `set1` when duplicate elements are encountered.
 {-# specialize: [1] #-}
-union {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
-  for (acc := set1) (x in set2) {
+unionLeft {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
+  for (acc := set2) (x in set1) {
     insert x acc
   };
 
+--- 𝒪(min(n,m) log min(n, m)). Returns a set containing the elements that are members of `set1` or `set2`.
+{-# specialize: [1] #-}
+union {A} {{Ord A}} (set1 set2 : AVLTree A) : AVLTree A :=
+  if
+    | height set1 < height set2 := unionLeft set1 set2
+    | else := unionLeft set2 set1;
+
+--- O(n log n). Returns a set containing the elements that are members of some set in `sets`.
+{-# specialize: [1, 2] #-}
+unions
+  {Container Elem}
+  {{Ord Elem}}
+  {{Foldable Container (AVLTree Elem)}}
+  (sets : Container)
+  : AVLTree Elem :=
+  for (acc := empty) (set in sets) {
+    union acc set
+  };
+
+--- O(n log n). If `set1` and `set2` are disjoint, then returns `ok set` where
+--- `set` is the union of `set1` and `set2`. If `set1` and `set2` are not
+--- disjoint, then returns `error x` where `x` is a common element.
+{-# specialize: [1] #-}
+disjointUnion {A} {{Ord A}} (set1 set2 : AVLTree A) : Result A (AVLTree A) :=
+  let
+    goUnion (set1 set2 : AVLTree A) : Result A (AVLTree A) :=
+      for (acc := ok set2) (x in set1) {
+        case acc of
+          | error _ := acc
+          | ok set :=
+            if
+              | isMember x set2 := error x
+              | else := ok (insert x set)
+      };
+  in if
+    | height set1 < height set2 := goUnion set1 set2
+    | else := goUnion set2 set1;
+
 syntax iterator all {init := 0; range := 1};
 --- 𝒪(𝓃). Returns ;true; if all elements of `set` satisfy `predicate`.
 {-# specialize: [1] #-}
@@ -352,7 +422,12 @@ filter {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : AVLTree A :=
   };
 
 syntax iterator partition {init := 0; range := 1};
-partition {A} {{Ord A}} (predicate : A -> Bool) (set : AVLTree A) : Pair (AVLTree A) (AVLTree A) :=
+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
@@ -398,7 +473,8 @@ toTree {A} : (set : AVLTree A) -> Maybe (Tree A)
     just (Tree.node element (catMaybes (toTree left :: toTree right :: nil)));
 
 --- Returns the textual representation of an ;AVLTree;.
-pretty {A} {{Show A}} (set : AVLTree A) : String := maybe "empty" Tree.treeToString (toTree set);
+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/Tree.juvix b/Stdlib/Data/Tree.juvix
index bdbf1fe6..56e135f3 100644
--- a/Stdlib/Data/Tree.juvix
+++ b/Stdlib/Data/Tree.juvix
@@ -13,7 +13,7 @@ Forest (A : Type) : Type := List (Tree A);
 type Tree (A : Type) :=
   node@{
     element : A;
-    children : List (Tree A)
+    children : List (Tree A);
   };
 
 terminating
@@ -32,4 +32,5 @@ drawForest {A} {{Show A}} (forest : Forest A) : List String :=
 
 treeToString {A} {{Show A}} (tree : Tree A) : String := unlines (draw tree);
 
-forestToString {A} {{Show A}} (forest : Forest A) : String := unlines (drawForest forest);
+forestToString {A} {{Show A}} (forest : Forest A) : String :=
+  unlines (drawForest forest);
diff --git a/Stdlib/Data/UnbalancedSet.juvix b/Stdlib/Data/UnbalancedSet.juvix
index 1f0b5dc4..a49bbf6b 100644
--- a/Stdlib/Data/UnbalancedSet.juvix
+++ b/Stdlib/Data/UnbalancedSet.juvix
@@ -10,7 +10,7 @@ open Tree using {BinaryTree; leaf; node};
 type UnbalancedSet (A : Type) :=
   mkUnbalancedSet@{
     order : Ord A;
-    tree : BinaryTree A
+    tree : BinaryTree A;
   };
 
 empty {A} {{order : Ord A}} : UnbalancedSet A := mkUnbalancedSet order leaf;
@@ -41,12 +41,14 @@ insert {A} (elem : A) (set : UnbalancedSet A) : UnbalancedSet A :=
               | Ord.GreaterThan := node l y (go r);
       in mkUnbalancedSet order (go tree);
 
-length {A} (set : UnbalancedSet A) : Nat := Tree.length (UnbalancedSet.tree set);
+length {A} (set : UnbalancedSet A) : Nat :=
+  Tree.length (UnbalancedSet.tree set);
 
-toList {A} (set : UnbalancedSet A) : List A := Tree.toList (UnbalancedSet.tree set);
+toList {A} (set : UnbalancedSet A) : List A :=
+  Tree.toList (UnbalancedSet.tree set);
 
 instance
 ordUnbalancedSetI {A} {{Ord A}} : Ord (UnbalancedSet A) :=
   mkOrd@{
-    cmp (s1 s2 : UnbalancedSet A) : Ordering := Ord.cmp (toList s1) (toList s2)
+    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 5602f05a..1bdb887c 100644
--- a/Stdlib/Data/Unit.juvix
+++ b/Stdlib/Data/Unit.juvix
@@ -13,19 +13,19 @@ import Stdlib.Trait.Foldable open;
 instance
 eqUnitI : Eq Unit :=
   mkEq@{
-    eq (_ _ : Unit) : Bool := true
+    eq (_ _ : Unit) : Bool := true;
   };
 
 instance
 ordUnitI : Ord Unit :=
   mkOrd@{
-    cmp (_ _ : Unit) : Ordering := Equal
+    cmp (_ _ : Unit) : Ordering := Equal;
   };
 
 instance
 showUnitI : Show Unit :=
   mkShow@{
-    show (_ : Unit) : String := "unit"
+    show (_ : Unit) : String := "unit";
   };
 
 {-# specialize: true, inline: case #-}
@@ -33,9 +33,17 @@ instance
 foldableUnitI : Foldable Unit Unit :=
   mkFoldable@{
     {-# inline: true #-}
-    rfor {Acc : Type} (fun : Acc -> Unit -> Acc) (initialValue : Acc) (_ : Unit) : Acc :=
-      fun initialValue unit;
+    rfor
+      {Acc : Type}
+      (fun : Acc -> Unit -> Acc)
+      (initialValue : Acc)
+      (_ : Unit)
+      : Acc := fun initialValue unit;
     {-# inline: true #-}
-    for {Acc : Type} (fun : Acc -> Unit -> Acc) (initialValue : Acc) (_ : Unit) : Acc :=
-      fun initialValue unit
+    for
+      {Acc : Type}
+      (fun : Acc -> Unit -> Acc)
+      (initialValue : Acc)
+      (_ : Unit)
+      : Acc := fun initialValue unit;
   };
diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix
index ff27d6b2..6a8f1cb6 100644
--- a/Stdlib/Trait/Applicative.juvix
+++ b/Stdlib/Trait/Applicative.juvix
@@ -15,19 +15,28 @@ 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
+    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 :=
-  ap (map λ{_ b := b} fa) fb;
+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 :=
-  map fun >> ap;
+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};
 mapA_
diff --git a/Stdlib/Trait/DivMod.juvix b/Stdlib/Trait/DivMod.juvix
index 7b92a89b..dbad0b34 100644
--- a/Stdlib/Trait/DivMod.juvix
+++ b/Stdlib/Trait/DivMod.juvix
@@ -6,7 +6,7 @@ type DivMod A :=
     {-# isabelle-operator: {name: "div", prec: 70, assoc: left} #-}
     div : A -> A -> A;
     {-# isabelle-operator: {name: "mod", prec: 70, assoc: left} #-}
-    mod : A -> A -> A
+    mod : A -> A -> A;
   };
 
 open DivMod public;
diff --git a/Stdlib/Trait/Foldable/Monomorphic.juvix b/Stdlib/Trait/Foldable/Monomorphic.juvix
index 50b843cd..da38c701 100644
--- a/Stdlib/Trait/Foldable/Monomorphic.juvix
+++ b/Stdlib/Trait/Foldable/Monomorphic.juvix
@@ -12,7 +12,7 @@ type Foldable (Container Elem : Type) :=
     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,10 +21,13 @@ 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
+    rfor := Poly.rfor;
   };
 
 {-# inline: true #-}
diff --git a/Stdlib/Trait/Foldable/Polymorphic.juvix b/Stdlib/Trait/Foldable/Polymorphic.juvix
index 55004fac..727dc740 100644
--- a/Stdlib/Trait/Foldable/Polymorphic.juvix
+++ b/Stdlib/Trait/Foldable/Polymorphic.juvix
@@ -10,7 +10,7 @@ type Foldable (F : Type -> Type) :=
     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;
diff --git a/Stdlib/Trait/Functor.juvix b/Stdlib/Trait/Functor.juvix
index d04faedd..56d7e8a0 100644
--- a/Stdlib/Trait/Functor.juvix
+++ b/Stdlib/Trait/Functor.juvix
@@ -2,4 +2,6 @@ module Stdlib.Trait.Functor;
 
 import Stdlib.Trait.Functor.Polymorphic open public;
 import Stdlib.Trait.Functor.Monomorphic as Monomorphic public;
-import Stdlib.Trait.Functor.Monomorphic open using {fromPolymorphicFunctor} public;
+import Stdlib.Trait.Functor.Monomorphic open using {
+  fromPolymorphicFunctor;
+} public;
diff --git a/Stdlib/Trait/Functor/Monomorphic.juvix b/Stdlib/Trait/Functor/Monomorphic.juvix
index 70a641f3..076fde2c 100644
--- a/Stdlib/Trait/Functor/Monomorphic.juvix
+++ b/Stdlib/Trait/Functor/Monomorphic.juvix
@@ -10,15 +10,16 @@ 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
+    map := Poly.map;
   };
 
 syntax operator <$> lapp;
diff --git a/Stdlib/Trait/Functor/Polymorphic.juvix b/Stdlib/Trait/Functor/Polymorphic.juvix
index 8a637efc..8b58bae0 100644
--- a/Stdlib/Trait/Functor/Polymorphic.juvix
+++ b/Stdlib/Trait/Functor/Polymorphic.juvix
@@ -9,18 +9,21 @@ 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} (fun : A -> B) (fa : F A) : F B := map fun fa;
+<$> {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/Integral.juvix b/Stdlib/Trait/Integral.juvix
index da871c45..313c6ff6 100644
--- a/Stdlib/Trait/Integral.juvix
+++ b/Stdlib/Trait/Integral.juvix
@@ -12,7 +12,7 @@ type Integral A :=
     {-# isabelle-operator: {name: "-", prec: 65, assoc: left} #-}
     - : A -> A -> A;
     builtin from-int
-    fromInt : Int -> A
+    fromInt : Int -> A;
   };
 
 open Integral using {fromInt; -} public;
diff --git a/Stdlib/Trait/Monad.juvix b/Stdlib/Trait/Monad.juvix
index 3632be52..9aec2e0d 100644
--- a/Stdlib/Trait/Monad.juvix
+++ b/Stdlib/Trait/Monad.juvix
@@ -8,13 +8,21 @@ type Monad (M : Type -> Type) :=
   mkMonad@{
     {{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/Numeric.juvix b/Stdlib/Trait/Numeric.juvix
index bba11955..6bdaf83e 100644
--- a/Stdlib/Trait/Numeric.juvix
+++ b/Stdlib/Trait/Numeric.juvix
@@ -8,7 +8,7 @@ type Numeric A :=
   mkNumeric@{
     integralI : Integral A;
     syntax operator / multiplicative;
-    / : A -> A -> A
+    / : A -> A -> A;
   };
 
 open Numeric using {/} public;
diff --git a/Stdlib/Trait/Ord.juvix b/Stdlib/Trait/Ord.juvix
index faa33a0f..d590a868 100644
--- a/Stdlib/Trait/Ord.juvix
+++ b/Stdlib/Trait/Ord.juvix
@@ -31,7 +31,7 @@ orderingEqI : Eq Ordering :=
       case ordering2 of
         | LessThan := isLessThan ordering1
         | Equal := isEqual ordering1
-        | GreaterThan := isGreaterThan ordering1
+        | GreaterThan := isGreaterThan ordering1;
   };
 
 --- A trait for defining a total order
diff --git a/test/Package.juvix b/test/Package.juvix
index ca94b3e0..8304ebad 100644
--- a/test/Package.juvix
+++ b/test/Package.juvix
@@ -6,8 +6,12 @@ package : Package :=
   defaultPackage@?{
     name := "stdlib-test";
     dependencies :=
-      [ path "../"
-      ; github "anoma" "juvix-quickcheck" "4242b864714f98947753544ea1b2cb435f6473d3"
-      ; github "anoma" "juvix-test" "85811914324b082549cb1f500323884442fc793c"
-      ]
+      [
+        path "../";
+        github
+          "anoma"
+          "juvix-quickcheck"
+          "4242b864714f98947753544ea1b2cb435f6473d3";
+        github "anoma" "juvix-test" "85811914324b082549cb1f500323884442fc793c";
+      ];
   };
diff --git a/test/Test.juvix b/test/Test.juvix
index 26084f70..5f467370 100644
--- a/test/Test.juvix
+++ b/test/Test.juvix
@@ -17,9 +17,11 @@ import Test.Map open using {suite as mapSuite};
 import Test.Queue open using {suite as queueSuite};
 import Test.UnbalancedSet open using {suite as unbalancedSetSuite};
 
-propReverseDoesNotChangeLength (xs : List Int) : Bool := length (reverse xs) == length xs;
+propReverseDoesNotChangeLength (xs : List Int) : Bool :=
+  length (reverse xs) == length xs;
 
-propReverseReverseIsIdentity (xs : List Int) : Bool := eqListInt xs (reverse (reverse xs));
+propReverseReverseIsIdentity (xs : List Int) : Bool :=
+  eqListInt xs (reverse (reverse xs));
 
 propTailLengthOneLess (xs : List Int) : Bool :=
   isEmpty xs || ofNat (length (tail xs)) == intSubNat (length xs) 1;
@@ -32,12 +34,15 @@ propSplitAtLength (n : Nat) (xs : List Int) : Bool :=
     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);
+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));
+      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;
 
@@ -56,7 +61,9 @@ propSort (sort : List Int -> List Int) (xs : List Int) : Bool :=
       | nil := true
       | (_ :: nil) := true
       | (x :: y :: xs) := x <= y && isSorted (y :: xs);
-  in length sorted == length xs && eqListInt sorted (sort sorted) && isSorted sorted;
+  in length sorted == length xs
+    && eqListInt sorted (sort sorted)
+    && isSorted sorted;
 
 propZip (xs ys : List Int) : Bool :=
   let
@@ -83,10 +90,12 @@ propSnoc (xs : List Int) (x : Int) : Bool :=
 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);
+  in length drop-n <= length xs
+    && eqListInt (drop n (drop n xs)) (drop (2 * n) xs);
 
 -- Assumption: The input list represents a rectangular matrix
-propTransposeMatrixId (xs : List (List Int)) : Bool := 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
 propTransposeMatrixDimensions (xs : List (List Int)) : Bool :=
@@ -107,7 +116,8 @@ propFoundElementSatisfiesPredicate (p : Int -> Bool) (xs : List Int) : Bool :=
     | just x := p x
     | nothing := true;
 
-propNonExistenceImpliesPredicateFalseForAll (p : Int -> Bool) (xs : List Int) : Bool :=
+propNonExistenceImpliesPredicateFalseForAll
+  (p : Int -> Bool) (xs : List Int) : Bool :=
   case find p xs of
     | just _ := true
     | nothing :=
@@ -115,7 +125,8 @@ propNonExistenceImpliesPredicateFalseForAll (p : Int -> Bool) (xs : List Int) :
         not (p x)
       };
 
-propFindConsistentWithSplitAt (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;
@@ -138,7 +149,8 @@ propFindWithAlwaysTrueIsJust (xs : List Int) : Bool :=
         | just _ := true
         | nothing := false;
 
-propFindWithAlwaysFalseIsNothing (xs : List Int) : Bool := find (const false) xs == nothing;
+propFindWithAlwaysFalseIsNothing (xs : List Int) : Bool :=
+  find (const false) xs == nothing;
 
 propResultErrorApplication (f : Int -> Int) (g : Int -> Int) (x : Int) : Bool :=
   handleResult f g (error x) == f x;
@@ -156,7 +168,8 @@ propResultIsOk (result : Result Int Bool) : Bool :=
     | error _ := not (isOk result)
     | ok _ := isOk result;
 
-propResultFromErrorDefault (defaultError : Int) (result : Result Int Bool) : Bool :=
+propResultFromErrorDefault
+  (defaultError : Int) (result : Result Int Bool) : Bool :=
   case result of
     | error x := fromError defaultError result == x
     | ok _ := fromError defaultError result == defaultError;
@@ -197,22 +210,29 @@ zipTest : QC.Test := QC.mkTest "zip properties" propZip;
 
 zipWithTest : QC.Test := QC.mkTest "zipWith properties" propZipWith;
 
-equalCompareToEqTest : QC.Test := QC.mkTest "equal Nats compare to EQ" propEqualCompareToEq;
+equalCompareToEqTest : QC.Test :=
+  QC.mkTest "equal Nats compare to EQ" propEqualCompareToEq;
 
 gcdNoCoprimeTest : QC.Test := QC.mkTest "no integers are coprime" propGcdBad;
 
 partitionTest : QC.Test :=
-  QC.mkTest "partition: recombination of the output equals the input" propPartition;
+  QC.mkTest
+    "partition: recombination of the output equals the input"
+    propPartition;
 
-testDistributive : QC.Test := QC.mkTest "all functions are distributive over +" propDistributive;
+testDistributive : QC.Test :=
+  QC.mkTest "all functions are distributive over +" propDistributive;
 
-reverseLengthTest : QC.Test := QC.mkTest "reverse preserves length" propReverseDoesNotChangeLength;
+reverseLengthTest : QC.Test :=
+  QC.mkTest "reverse preserves length" propReverseDoesNotChangeLength;
 
 reverseReverseIdTest : QC.Test :=
   QC.mkTest "reverse of reverse is identity" propReverseReverseIsIdentity;
 
 splitAtRecombineTest : QC.Test :=
-  QC.mkTest "splitAt: recombination of the output is equal to the input list" propSplitAtRecombine;
+  QC.mkTest
+    "splitAt: recombination of the output is equal to the input list"
+    propSplitAtRecombine;
 
 splitAtLengthTest : QC.Test :=
   QC.mkTest
@@ -225,7 +245,9 @@ mergeSumLengthsTest : QC.Test :=
     propMergeSumLengths;
 
 tailLengthOneLessTest : QC.Test :=
-  QC.mkTest "tail: length of output is one less than input unless empty" propTailLengthOneLess;
+  QC.mkTest
+    "tail: length of output is one less than input unless empty"
+    propTailLengthOneLess;
 
 transposeMatrixIdTest : QC.Test :=
   QC.mkTest
@@ -240,7 +262,9 @@ transposeMatrixDimentionsTest : QC.Test :=
     propTransposeMatrixDimensions;
 
 findFoundElementSatisfiesPredicate : QC.Test :=
-  QC.mkTest "find: found element satisfies predicate" propFoundElementSatisfiesPredicate;
+  QC.mkTest
+    "find: found element satisfies predicate"
+    propFoundElementSatisfiesPredicate;
 
 findNonExistenceImpliesPredicateFalseForAll : QC.Test :=
   QC.mkTest
@@ -254,10 +278,14 @@ findOnEmptyListIsNothing : QC.Test :=
   QC.mkTest "find: called with empty list is nothing" propFindWithEmptyList;
 
 findWithAlwaysTrueIsJust : QC.Test :=
-  QC.mkTest "find: always true predicate returns just" propFindWithAlwaysTrueIsJust;
+  QC.mkTest
+    "find: always true predicate returns just"
+    propFindWithAlwaysTrueIsJust;
 
 findWithAlwaysFalseIsNothing : QC.Test :=
-  QC.mkTest "find: always false predicate returns nothing" propFindWithAlwaysFalseIsNothing;
+  QC.mkTest
+    "find: always false predicate returns nothing"
+    propFindWithAlwaysFalseIsNothing;
 
 resultResultErrorApplication : QC.Test :=
   QC.mkTest "result: result error application" propResultErrorApplication;
@@ -265,17 +293,22 @@ resultResultErrorApplication : QC.Test :=
 resultResultOkApplication : QC.Test :=
   QC.mkTest "result: result ok application" propResultOkApplication;
 
-resultIsError : QC.Test := QC.mkTest "result: isError detects error" propResultIsError;
+resultIsError : QC.Test :=
+  QC.mkTest "result: isError detects error" propResultIsError;
 
 resultIsOk : QC.Test := QC.mkTest "result: isOk detects ok" propResultIsOk;
 
-resultFromError : QC.Test := QC.mkTest "result: fromError uses default" propResultFromErrorDefault;
+resultFromError : QC.Test :=
+  QC.mkTest "result: fromError uses default" propResultFromErrorDefault;
 
-resultFromOk : QC.Test := QC.mkTest "result: fromOk uses default" propResultFromOkDefault;
+resultFromOk : QC.Test :=
+  QC.mkTest "result: fromOk uses default" propResultFromOkDefault;
 
-resultResultToMaybe : QC.Test := QC.mkTest "result: resultToMaybe" propResultToMaybe;
+resultResultToMaybe : QC.Test :=
+  QC.mkTest "result: resultToMaybe" propResultToMaybe;
 
-resultMaybeToResult : QC.Test := QC.mkTest "result: maybeToResult" propMaybeToResult;
+resultMaybeToResult : QC.Test :=
+  QC.mkTest "result: maybeToResult" propMaybeToResult;
 
 resultMapError : QC.Test := QC.mkTest "result: mapError" propResultMapError;
 
@@ -289,42 +322,44 @@ main : IO :=
         in QC.runTestsIO
             100
             seedNat
-            [ partitionTest
-            ; reverseLengthTest
-            ; reverseReverseIdTest
-            ; splitAtRecombineTest
-            ; splitAtLengthTest
-            ; mergeSumLengthsTest
-            ; tailLengthOneLessTest
-            ; equalCompareToEqTest
-            ; zipTest
-            ; zipWithTest
-            ; snocTest
-            ; dropTest
-            ; sortTest "mergeSort" mergeSort
-            ; sortTest "quickSort" quickSort
-            ; transposeMatrixIdTest
-            ; transposeMatrixDimentionsTest
-            ; findFoundElementSatisfiesPredicate
-            ; findNonExistenceImpliesPredicateFalseForAll
-            ; findConsistentWithSplitAt
-            ; findOnEmptyListIsNothing
-            ; findWithAlwaysTrueIsJust
-            ; findWithAlwaysFalseIsNothing
+            [
+              partitionTest;
+              reverseLengthTest;
+              reverseReverseIdTest;
+              splitAtRecombineTest;
+              splitAtLengthTest;
+              mergeSumLengthsTest;
+              tailLengthOneLessTest;
+              equalCompareToEqTest;
+              zipTest;
+              zipWithTest;
+              snocTest;
+              dropTest;
+              sortTest "mergeSort" mergeSort;
+              sortTest "quickSort" quickSort;
+              transposeMatrixIdTest;
+              transposeMatrixDimentionsTest;
+              findFoundElementSatisfiesPredicate;
+              findNonExistenceImpliesPredicateFalseForAll;
+              findConsistentWithSplitAt;
+              findOnEmptyListIsNothing;
+              findWithAlwaysTrueIsJust;
+              findWithAlwaysFalseIsNothing;
             ]
           >>> QC.runTestsIO
             100
             seedNat
-            [ resultResultErrorApplication
-            ; resultResultOkApplication
-            ; resultIsError
-            ; resultIsOk
-            ; resultFromError
-            ; resultFromOk
-            ; resultResultToMaybe
-            ; resultMaybeToResult
-            ; resultMapError
-            ; resultMapOk
+            [
+              resultResultErrorApplication;
+              resultResultOkApplication;
+              resultIsError;
+              resultIsOk;
+              resultFromError;
+              resultFromOk;
+              resultResultToMaybe;
+              resultMaybeToResult;
+              resultMapError;
+              resultMapOk;
             ]}
     >>> runTestSuite avlSuite
     >>> runTestSuite mapSuite
diff --git a/test/Test/AVL.juvix b/test/Test/AVL.juvix
index 15b502a0..a82b3326 100644
--- a/test/Test/AVL.juvix
+++ b/test/Test/AVL.juvix
@@ -20,15 +20,20 @@ mkTests {A} (descr : TestDescr A) : List Test :=
           | 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 (Internal.isBalanced testSet))
+      in [
+           testCase
+             (mkTitle "size")
+             (assertEqual sizeMsg (size testSet) testLen);
+           testCase
+             (mkTitle "balanced")
+             (assertTrue balanceMsg (Internal.isBalanced testSet));
          ];
 
 type TestDescr (A : Type) :=
   mkTestDescr@{
     testTitle : String;
     testLen : Nat;
-    testSet : AVLTree A
+    testSet : AVLTree A;
   };
 
 s1Tree : AVLTree Nat := fromList [1; 2; 8; 3; 3; 2; 9];
@@ -43,79 +48,116 @@ s2Delete : TestDescr Nat :=
   mkTestDescr@{
     testTitle := TestDescr.testTitle s2 ++str "-delete";
     testLen := sub (TestDescr.testLen s2) 2;
-    testSet := deleteMany [1; 8] (TestDescr.testSet s2)
+    testSet := deleteMany [1; 8] (TestDescr.testSet s2);
   };
 
 s2DeleteWith : TestDescr Box :=
   mkTestDescr@{
     testTitle := TestDescr.testTitle s2 ++str "-delete-with";
     testLen := sub (TestDescr.testLen s2) 2;
-    testSet := deleteManyWith Box.b [1; 8] (TestDescr.testSet s2 |> AVL.map mkBox)
+    testSet :=
+      deleteManyWith Box.b [1; 8] (TestDescr.testSet s2 |> AVL.map mkBox);
   };
 
 s3 : TestDescr Nat :=
   mkTestDescr@{
     testTitle := "s3";
     testLen := 6;
-    testSet := fromList [5; 4; 3; 2; 1; 0]
+    testSet := fromList [5; 4; 3; 2; 1; 0];
   };
 
 s4 : TestDescr Nat :=
   mkTestDescr@{
     testTitle := "s4";
     testLen := 5;
-    testSet := fromList [1; 2; 3; 4; 5]
+    testSet := fromList [1; 2; 3; 4; 5];
   };
 
 tests : List Test :=
-  [ testCase "s1-member" (assertTrue "isMember 3 s1" (AVL.isMember 3 s1Tree))
-  ; testCase
-    "s1-s2-intersection"
-    (assertEqual "intersection s1Tree s2Tree" (intersection s1Tree s2Tree) (fromList [1; 2; 3; 8]))
-  ; testCase
-    "s1-s2-difference"
-    (assertEqual "difference s1Tree s2Tree" (difference s1Tree s2Tree) (fromList [9]))
-  ; testCase
-    "s1-s2-union"
-    (assertEqual "union s1Tree s2Tree" (union s1Tree s2Tree) (fromList [0; 1; 2; 3; 4; 8; 9]))
-  ; testCase
-    "s2-filter"
-    (assertEqual "filter (> 3) s2" [0; 1; 2] (AVL.filter ((>) 3) s2Tree |> AVL.toList))
-  ; testCase "s2-all" (assertTrue "all (> 9) s2" (AVL.all ((>) 9) s2Tree))
-  ; testCase "s2-any" (assertTrue "any (< 3) s2" (AVL.any ((<) 3) s2Tree))
-  ; testCase
-    "s2-partition"
-    (assertEqual
-      "partition (< 3) s2"
-      ([0; 1; 2], [3; 4; 8])
-      (AVL.partition ((>) 3) s2Tree |> both AVL.toList))
-  ; testCase "s2-lookup" (assertJust "lookup 4 s2" (lookup 4 s2Tree))
-  ; testCase "s2-lookup" (assertNothing (const "lookup 5 s2") (lookup 5 s2Tree))
-  ; testCase "s2-lookup" (assertNothing (const "lookup 6 s2") (lookup 6 s2Tree))
-  ; testCase "s1-s2-not-isSubset" (assertFalse "isSubset s1 s2" (isSubset s1Tree s2Tree))
-  ; testCase "s2-s1-not-isSubset" (assertFalse "isSubset s2 s1" (isSubset s2Tree s1Tree))
-  ; testCase
-    "singleton-s2-isSubset"
-    (assertTrue "isSubset (singleton 1) s2" (isSubset (singleton 1) s2Tree))
-  ; testCase "s2-foldr" (assertEqual "foldr (+) 0 s2" 18 (AVL.foldr (+) 0 s2Tree))
-  ; testCase "s2-foldl" (assertEqual "foldl (+) 0 s2" 18 (AVL.foldl (+) 0 s2Tree))
-  ; testCase
-    "s2-map"
-    (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
-    }
-  ; 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
-    }
+  [
+    testCase "s1-member" (assertTrue "isMember 3 s1" (AVL.isMember 3 s1Tree));
+    testCase
+      "s1-s2-intersection"
+      (assertEqual
+        "intersection s1Tree s2Tree"
+        (intersection s1Tree s2Tree)
+        (fromList [1; 2; 3; 8]));
+    testCase
+      "s1-s2-difference"
+      (assertEqual
+        "difference s1Tree s2Tree"
+        (difference s1Tree s2Tree)
+        (fromList [9]));
+    testCase
+      "s1-s2-union"
+      (assertEqual
+        "union s1Tree s2Tree"
+        (union s1Tree s2Tree)
+        (fromList [0; 1; 2; 3; 4; 8; 9]));
+    testCase
+      "s2-filter"
+      (assertEqual
+        "filter (> 3) s2"
+        [0; 1; 2]
+        (AVL.filter ((>) 3) s2Tree |> AVL.toList));
+    testCase "s2-all" (assertTrue "all (> 9) s2" (AVL.all ((>) 9) s2Tree));
+    testCase "s2-any" (assertTrue "any (< 3) s2" (AVL.any ((<) 3) s2Tree));
+    testCase
+      "s2-partition"
+      (assertEqual
+        "partition (< 3) s2"
+        ([0; 1; 2], [3; 4; 8])
+        (AVL.partition ((>) 3) s2Tree |> both AVL.toList));
+    testCase "s2-lookup" (assertJust "lookup 4 s2" (lookup 4 s2Tree));
+    testCase
+      "s2-lookup"
+      (assertNothing (const "lookup 5 s2") (lookup 5 s2Tree));
+    testCase
+      "s2-lookup"
+      (assertNothing (const "lookup 6 s2") (lookup 6 s2Tree));
+    testCase
+      "s1-s2-not-isSubset"
+      (assertFalse "isSubset s1 s2" (isSubset s1Tree s2Tree));
+    testCase
+      "s2-s1-not-isSubset"
+      (assertFalse "isSubset s2 s1" (isSubset s2Tree s1Tree));
+    testCase
+      "singleton-s2-isSubset"
+      (assertTrue "isSubset (singleton 1) s2" (isSubset (singleton 1) s2Tree));
+    testCase
+      "s2-foldr"
+      (assertEqual "foldr (+) 0 s2" 18 (AVL.foldr (+) 0 s2Tree));
+    testCase
+      "s2-foldl"
+      (assertEqual "foldl (+) 0 s2" 18 (AVL.foldl (+) 0 s2Tree));
+    testCase
+      "s2-map"
+      (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
+      };
+    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
+      };
+    testCase "disjointUnion disjoint"
+      <| assertEqual "disjointUnion for disjoint" (ok (fromList [0; 1; 2; 3]))
+      <| disjointUnion (fromList [0; 3]) (fromList [1; 2]);
+    testCase "disjointUnion not disjoint"
+      <| assertEqual "disjointUnion for non-disjoint" (error 0)
+      <| disjointUnion (fromList [0; 3]) (fromList [0; 1; 2]);
   ]
     ++ concatMap mkTests [s1; s2; s3; s4; s2Delete];
 
 suite : TestSuite := testSuite "AVL Set" tests;
 
 main : IO :=
-  printStringLn (pretty s1Tree) >>> printStringLn (prettyDebug s1Tree) >>> runTestSuite suite;
+  printStringLn (pretty s1Tree)
+    >>> printStringLn (prettyDebug s1Tree)
+    >>> runTestSuite suite;
diff --git a/test/Test/Arb.juvix b/test/Test/Arb.juvix
index c7a2521b..2b17063a 100644
--- a/test/Test/Arb.juvix
+++ b/test/Test/Arb.juvix
@@ -6,7 +6,8 @@ import Test.QuickCheck.Arbitrary open;
 import Test.QuickCheck.Gen open;
 import Data.Random open;
 
-arbitrarySizedList {A} (size : Nat) (arbitraryA : Arbitrary A) : Arbitrary (List A) :=
+arbitrarySizedList
+  {A} (size : Nat) (arbitraryA : Arbitrary A) : Arbitrary (List A) :=
   case arbitraryA of
     mkArbitrary g :=
       mkArbitrary
diff --git a/test/Test/Map.juvix b/test/Test/Map.juvix
index 7e83057b..1a1f596c 100644
--- a/test/Test/Map.juvix
+++ b/test/Test/Map.juvix
@@ -9,82 +9,169 @@ import Stdlib.Data.Set as Set open using {Set};
 tests : List Test :=
   let
     m : Map Nat String := Map.insert 2 "two" (Map.insert 1 "one" Map.empty);
+    m1 : Map Nat Nat := Map.insert 4 5 (Map.insert 1 3 Map.empty);
     m2 : Map Nat Nat := Map.insert 3 4 (Map.insert 1 2 Map.empty);
-    assertEqListPair (actual : List (Pair Nat Nat)) (expected : List (Pair Nat Nat)) : Assertion :=
+    m3 : Map Nat Nat := Map.insert 0 0 Map.empty;
+    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))
-     ; testCase
-       "Map.lookup available key"
-       (assertJust "could not find expected key" (Map.lookup 2 m))
-     ; testCase
-       "Map.delete exiting key"
-       (assertNothing (const "expected deleted key to be missing") (Map.delete 2 m |> Map.lookup 2))
-     ; testCase
-       "Map.delete missing key"
-       (assertEqual "expected maps to be equal" m (Map.delete 100 m))
-     ; testCase
-       "Map.length computes the number of keys in the map"
-       (assertEqual "expected length 2" (Map.size m) 2)
-     ; testCase
-       "Map.toList computes the expected members"
-       (assertEqListPair (Map.toList m2) [1, 2; 3, 4])
-     ; testCase
-       "Map.insert-with replaces duplicates using merge function"
-       (assertEqListPair (Map.toList (Map.insertWith (+) 1 3 m2)) [1, 5; 3, 4])
-     ; testCase
-       "Map.fromListWith de-duplicates using merge function"
-       (assertEqListPair (Map.toList (Map.fromListWith (+) [1, 1; 1, 2])) [1, 3])
-     ; testCase
-       "Map.fromList can be used to create the empty Map"
-       (assertEqListPair (Map.toList (Map.fromList nil)) (nil))
-     ; testCase
-       "Map.fromList overwrites duplicates"
-       (assertEqListPair (Map.toList (Map.fromList [1, 1; 1, 2])) [1, 2])
-     ; testCase
-       "Map.fromList distinct keys"
-       (assertEqListPair (Map.toList (Map.fromList [1, 1; 2, 2])) [1, 1; 2, 2])
-     ; testCase
-       "Map.fromSet"
-       (assertEqListPair (Map.toList (Map.fromSet id (Set.fromList [1; 2; 3]))) [1, 1; 2, 2; 3, 3])
-     ; testCase "Map.keys" (assertEqual "expected keys" (Map.keys m) [1; 2])
-     ; testCase "Map.values" (assertEqual "expected values" (Map.values m) ["one"; "two"])
-     ; testCase "Map.keySet" (assertEqual "expected key set" (Map.keySet m) (Set.fromList [1; 2]))
-     ; testCase
-       "Map.valueSet"
-       (assertEqual "expected value set" (Map.valueSet m2) (Set.fromList [2; 4]))
-     ; testCase
-       "Map.isEmpty"
-       (assertEqual "expected empty map" (Map.isEmpty (Map.empty {Nat} {Nat})) true)
-     ; testCase "Map.isEmpty" (assertEqual "expected non-empty map" (Map.isEmpty m) false)
-     ; testCase "Map.isMember" (assertEqual "expected member" (Map.isMember 1 m) true)
-     ; 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])
-     ; testCase
-       "Map.partition"
-       (assertEqual
-         "expected partition"
-         ([1, 2], [3, 4])
-         (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])
-     ; 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.foldl"
-       (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)
-     ; testCase "Map.singleton" (assertEqListPair (Map.toList (Map.singleton 1 2)) [1, 2])
+  in [
+       testCase
+         "Map.lookup missing key"
+         (assertNothing
+           (const "found a key expected to be missing")
+           (Map.lookup 10 m));
+       testCase
+         "Map.lookup available key"
+         (assertJust "could not find expected key" (Map.lookup 2 m));
+       testCase
+         "Map.delete exiting key"
+         (assertNothing
+           (const "expected deleted key to be missing")
+           (Map.delete 2 m |> Map.lookup 2));
+       testCase
+         "Map.delete missing key"
+         (assertEqual "expected maps to be equal" m (Map.delete 100 m));
+       testCase
+         "Map.length computes the number of keys in the map"
+         (assertEqual "expected length 2" (Map.size m) 2);
+       testCase
+         "Map.toList computes the expected members"
+         (assertEqListPair (Map.toList m2) [1, 2; 3, 4]);
+       testCase
+         "Map.insert-with replaces duplicates using merge function"
+         (assertEqListPair
+           (Map.toList (Map.insertWith (+) 1 3 m2))
+           [1, 5; 3, 4]);
+       testCase
+         "Map.fromListWith de-duplicates using merge function"
+         (assertEqListPair
+           (Map.toList (Map.fromListWith (+) [1, 1; 1, 2]))
+           [1, 3]);
+       testCase
+         "Map.fromList can be used to create the empty Map"
+         (assertEqListPair (Map.toList (Map.fromList nil)) (nil));
+       testCase
+         "Map.fromList overwrites duplicates"
+         (assertEqListPair (Map.toList (Map.fromList [1, 1; 1, 2])) [1, 2]);
+       testCase
+         "Map.fromList distinct keys"
+         (assertEqListPair
+           (Map.toList (Map.fromList [1, 1; 2, 2]))
+           [1, 1; 2, 2]);
+       testCase
+         "Map.fromSetWithFun"
+         (assertEqListPair
+           (Map.toList (Map.fromSetWithFun id (Set.fromList [1; 2; 3])))
+           [1, 1; 2, 2; 3, 3]);
+       testCase
+         "Map.fromSet"
+         (assertEqListPair
+           (Map.toList (Map.fromSet (Set.fromList [1, 1; 2, 2; 3, 3])))
+           [1, 1; 2, 2; 3, 3]);
+       testCase "Map.keys" (assertEqual "expected keys" (Map.keys m) [1; 2]);
+       testCase
+         "Map.values"
+         (assertEqual "expected values" (Map.values m) ["one"; "two"]);
+       testCase
+         "Map.keySet"
+         (assertEqual "expected key set" (Map.keySet m) (Set.fromList [1; 2]));
+       testCase
+         "Map.valueSet"
+         (assertEqual
+           "expected value set"
+           (Map.valueSet m2)
+           (Set.fromList [2; 4]));
+       testCase
+         "Map.isEmpty"
+         (assertEqual
+           "expected empty map"
+           (Map.isEmpty (Map.empty {Nat} {Nat}))
+           true);
+       testCase
+         "Map.isEmpty"
+         (assertEqual "expected non-empty map" (Map.isEmpty m) false);
+       testCase
+         "Map.isMember"
+         (assertEqual "expected member" (Map.isMember 1 m) true);
+       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]);
+       testCase
+         "Map.partition"
+         (assertEqual
+           "expected partition"
+           ([1, 2], [3, 4])
+           (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]);
+       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.foldl"
+         (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);
+       testCase
+         "Map.singleton"
+         (assertEqListPair (Map.toList (Map.singleton 1 2)) [1, 2]);
+       testCase
+         "Map.union"
+         (assertEqListPair (Map.toList (Map.union m2 m3)) [0, 0; 1, 2; 3, 4]);
+       testCase
+         "Map.unionLeft"
+         (assertEqListPair
+           (Map.toList (Map.unionLeft m1 m2))
+           [1, 3; 3, 4; 4, 5]);
+       testCase
+         "Map.intersection"
+         (assertEqListPair (Map.toList (Map.intersection m1 m2)) [1, 3]);
+       testCase
+         "Map.difference"
+         (assertEqListPair (Map.toList (Map.difference m1 m2)) [4, 5]);
+       testCase
+         "Map.disjointUnion non-disjoint"
+         (assertEqual
+           "Map.disjointUnion non-disjoint"
+           (Map.disjointUnion m1 m2)
+           (error 1));
+       testCase
+         "Map.disjointUnion disjoint"
+         (assertEqual
+           "Map.disjointUnion disjoint"
+           (Map.disjointUnion
+             (Map.fromList [1, 1; 2, 2])
+             (Map.fromList [3, 3; 4, 4]))
+           (ok (Map.fromList [1, 1; 2, 2; 3, 3; 4, 4])));
      ];
 
 suite : TestSuite := testSuite "Map" tests;
diff --git a/test/Test/Queue.juvix b/test/Test/Queue.juvix
index dee7767b..65fbdbb5 100644
--- a/test/Test/Queue.juvix
+++ b/test/Test/Queue.juvix
@@ -22,21 +22,27 @@ tests : List Test :=
   let
     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])
-     ; testCase
-       "Queue.head should return first element"
-       (assertEqual "head of queue q3" (head q3) (just 1))
-     ; testCase
-       "Queue.fromList composes with toList should be the identity"
-       (assertEqual "fromList . toList should be the identity" (toList >> fromList <| q3) q3)
-     ; testCase
-       "Queue.pop should remove first element"
-       (assertEqual "pop of queue q3" (pop q3) (just (1, fromList [2; 3])))
-     ; testCase
-       "Queue.tail should return queue without first element"
-       (assertEqual "tail of queue q3" (tail q3) ((fromList >> just) [2; 3]))
+  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]);
+       testCase
+         "Queue.head should return first element"
+         (assertEqual "head of queue q3" (head q3) (just 1));
+       testCase
+         "Queue.fromList composes with toList should be the identity"
+         (assertEqual
+           "fromList . toList should be the identity"
+           (toList >> fromList <| q3)
+           q3);
+       testCase
+         "Queue.pop should remove first element"
+         (assertEqual "pop of queue q3" (pop q3) (just (1, fromList [2; 3])));
+       testCase
+         "Queue.tail should return queue without first element"
+         (assertEqual "tail of queue q3" (tail q3) ((fromList >> just) [2; 3]));
      ];
 
 suite : TestSuite := testSuite "Queue" tests;
diff --git a/test/Test/UnbalancedSet.juvix b/test/Test/UnbalancedSet.juvix
index 3a54bb03..cdd5bf8e 100644
--- a/test/Test/UnbalancedSet.juvix
+++ b/test/Test/UnbalancedSet.juvix
@@ -10,21 +10,28 @@ open Set using {UnbalancedSet};
 
 tests : List Test :=
   let
-    s : UnbalancedSet Nat := Set.insert 1 (Set.insert 3 (Set.insert 2 (Set.insert 1 Set.empty)));
+    s : UnbalancedSet Nat :=
+      Set.insert 1 (Set.insert 3 (Set.insert 2 (Set.insert 1 Set.empty)));
     setInSet : UnbalancedSet (UnbalancedSet Nat) := Set.insert s Set.empty;
-  in [ testCase
-       "Set.length computes the expected size"
-       (assertEqual "unexpected size" (Set.length s) 3)
-     ; testCase
-       "Set.to-list computes the expected members"
-       (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.isMember 1 s))
-     ; testCase
-       "Set.member? computes false for unexpected member"
-       (assertFalse "unexpected member is present" (Set.isMember 0 s))
-     ; testCase "setInSet has length 1" (assertEqual "unexpected size" (Set.length setInSet) 1)
+  in [
+       testCase
+         "Set.length computes the expected size"
+         (assertEqual "unexpected size" (Set.length s) 3);
+       testCase
+         "Set.to-list computes the expected members"
+         (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.isMember 1 s));
+       testCase
+         "Set.member? computes false for unexpected member"
+         (assertFalse "unexpected member is present" (Set.isMember 0 s));
+       testCase
+         "setInSet has length 1"
+         (assertEqual "unexpected size" (Set.length setInSet) 1);
      ];
 
 suite : TestSuite := testSuite "UnbalancedSet" tests;
diff --git a/test/juvix.lock.yaml b/test/juvix.lock.yaml
deleted file mode 100644
index b8049268..00000000
--- a/test/juvix.lock.yaml
+++ /dev/null
@@ -1,28 +0,0 @@
-# This file was autogenerated by Juvix version 0.6.6.
-# Do not edit this file manually.
-
-version: 2
-checksum: fbbd33d3d068b3369d271021b23b0407838642655173d086f1c81ead9bb338c8
-dependencies:
-- path: ../
-  dependencies: []
-- git:
-    name: anoma_juvix-quickcheck
-    ref: 4242b864714f98947753544ea1b2cb435f6473d3
-    url: https://github.com/anoma/juvix-quickcheck
-  dependencies:
-  - git:
-      name: anoma_juvix-stdlib
-      ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6
-      url: https://github.com/anoma/juvix-stdlib
-    dependencies: []
-- git:
-    name: anoma_juvix-test
-    ref: 85811914324b082549cb1f500323884442fc793c
-    url: https://github.com/anoma/juvix-test
-  dependencies:
-  - git:
-      name: anoma_juvix-stdlib
-      ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6
-      url: https://github.com/anoma/juvix-stdlib
-    dependencies: []