Refactorings and function removals

Stdlib/Data/List.juvix

@@ -9,18 +9,12 @@ import Stdlib.Trait.Eq open;
 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;
 };
 
---- 𝒪(1). Partial function that returns the first element of a ;List;.
-phead {A} {{Partial}} : List A -> A
-  | (x :: _) := x
-  | nil := fail "head: empty list";
-
 {-# specialize: true, inline: case #-}
 instance
 eqListI {A} {{Eq A}} : Eq (List A) :=

Stdlib/Data/List/Base.juvix

@@ -34,7 +34,7 @@ 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 :=
+listFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : B :=
   listRfor (flip fun) acc list;
 
 --- Left-associative and tail-recursive fold.
@@ -134,13 +134,10 @@ syntax operator ++ cons;
   | nil ys := ys
   | (x :: xs) ys := x :: xs ++ ys;
 
---- 𝒪(𝓃). Append an element.
-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;
+  listFoldr (++) nil listOfLists;
 
 --- 𝒪(𝓃). Inserts the given separator before every element in the given ;List;.
 prependToAll {A} (separator : A) : (list : List A) -> List A

Stdlib/Data/Map.juvix

@@ -14,7 +14,6 @@ import Stdlib.Trait.Ord open;
 import Stdlib.Function open;
 
 import Stdlib.Data.Set as Set open using {Set};
-import Stdlib.Data.Set.AVL as AVL open using {AVLTree};
 
 import Stdlib.Data.BinaryTree as Tree;
 
@@ -40,9 +39,9 @@ bindingKeyOrdering {Key Value} {{Ord Key}} : Ord (Binding Key Value) :=
     cmp (b1 b2 : Binding Key Value) : Ordering := Ord.cmp (key b1) (key b2);
   };
 
-type Map Key Value := mkMap (AVLTree (Binding Key Value));
+type Map Key Value := mkMap (Set (Binding Key Value));
 
-empty {Key Value} : Map Key Value := mkMap AVL.empty;
+empty {Key Value} : Map Key Value := mkMap Set.empty;
 
 {-# specialize: [1, fun] #-}
 insertWith