diff --git a/Algorithm.lean b/Algorithm.lean
index 5ff01f9..0c3f5b6 100644
--- a/Algorithm.lean
+++ b/Algorithm.lean
@@ -1,6 +1,6 @@
 import Algorithm.Algebra.BigOperators.DFinsupp'
-import Algorithm.Data.Classes.AssocArray
 import Algorithm.Data.Classes.Bag
+import Algorithm.Data.Classes.DefaultDict
 import Algorithm.Data.Classes.Dict
 import Algorithm.Data.Classes.Erase
 import Algorithm.Data.Classes.GetElem
diff --git a/Algorithm/Data/Classes/AssocArray.lean b/Algorithm/Data/Classes/DefaultDict.lean
similarity index 72%
rename from Algorithm/Data/Classes/AssocArray.lean
rename to Algorithm/Data/Classes/DefaultDict.lean
index c89aa33..dbfecf8 100644
--- a/Algorithm/Data/Classes/AssocArray.lean
+++ b/Algorithm/Data/Classes/DefaultDict.lean
@@ -7,60 +7,40 @@ import Algorithm.Data.Classes.GetElem
 import Algorithm.Data.DFinsupp'.Defs
 import Mathlib.Data.Setoid.Basic
 
-universe u v
-
 namespace Vector
 variable {α : Type*} {n : ℕ}
 
 set_option linter.unusedVariables false in -- TODO: generalize
 @[nolint unusedArguments]
-protected abbrev WithDefault (α : Type u) (n : Nat) (f : Fin n → α) := Vector α n
-
-instance {α n f} : Inhabited (Vector.WithDefault α n f) where
-  default := .ofFn f
-
-@[simp]
-lemma get_default {f} : (default : Vector.WithDefault α n f).get = f := by
-  ext i
-  exact getElem_ofFn i.2
+protected abbrev WithDefault (α : Type*) (n : Nat) (f : Fin n → α) := Vector α n
 
 end Vector
 
-class AssocDArray.ReadOnly (C : Type*) (ι : outParam Type*)
+class DefaultDict.ReadOnly (C : Type*) (ι : outParam Type*)
     (α : outParam Type*) (d : outParam <| ι → α) extends
     GetElemAllValid C ι α where
   toDFinsupp' : C → Π₀' i, [α, d i]
   coe_toDFinsupp'_eq_getElem : ∀ a, ⇑(toDFinsupp' a) = (a[·])
-export AssocDArray.ReadOnly (toDFinsupp' coe_toDFinsupp'_eq_getElem)
+export DefaultDict.ReadOnly (toDFinsupp' coe_toDFinsupp'_eq_getElem)
 
-/-- `AssocDArray C ι α d` is a data structure that acts like a finitely supported function
+/-- `DefaultDict C ι α d` is a data structure that acts like a finitely supported function
   `Π₀' i, [α, d i]` with single point update operation. -/
-class AssocDArray (C : Type*) [Inhabited C] (ι : outParam Type*)
+class DefaultDict (C : Type*) [Inhabited C] (ι : outParam Type*)
     (α : outParam Type*) (d : outParam <| ι → α) extends
-    AssocDArray.ReadOnly C ι α d, GetSetElemAllValid C ι α where
+    DefaultDict.ReadOnly C ι α d, GetSetElemAllValid C ι α where
   getElem_default i : (default : C)[i] = d i
 
-abbrev AssocArray.ReadOnly (C : Type*) (ι : outParam Type*)
-    (α : outParam Type*) (d : outParam α) :=
-  AssocDArray.ReadOnly C ι α (fun _ ↦ d)
-
-/-- `AssocArray C ι α d` is a data structure that acts like a finitely supported function
-  `ι →₀' [α, d]` with single point update operation. -/
-abbrev AssocArray (C : Type*) [Inhabited C] (ι : outParam Type*)
-    (α : outParam Type*) (d : outParam α) :=
-  AssocDArray C ι α (fun _ ↦ d)
-
-attribute [simp] AssocDArray.getElem_default coe_toDFinsupp'_eq_getElem
+attribute [simp] DefaultDict.getElem_default coe_toDFinsupp'_eq_getElem
 
 section AssocDArray
 
 variable {C ι α : Type*} {d : ι → α}
 
-variable [Inhabited C] [AssocDArray C ι α d]
+variable [Inhabited C] [DefaultDict C ι α d]
 
 instance : OfFn C ι α d where
   ofFn := default
-  getElem_ofFn i := AssocDArray.getElem_default i
+  getElem_ofFn i := DefaultDict.getElem_default i
 
 lemma toDFinsupp'_apply_eq_getElem (a : C) (i : ι) : toDFinsupp' a i = a[i] := by simp
 
@@ -79,7 +59,15 @@ end AssocDArray
 namespace Vector.WithDefault
 variable {α : Type*} {n : ℕ} {f : Fin n → α}
 
-instance : AssocDArray (Vector.WithDefault α n f) (Fin n) α f where
+instance {α n f} : Inhabited (Vector.WithDefault α n f) where
+  default := .ofFn f
+
+@[simp]
+lemma get_default {f} : (default : Vector.WithDefault α n f).get = f := by
+  ext i
+  exact getElem_ofFn i.2
+
+instance : DefaultDict (Vector.WithDefault α n f) (Fin n) α f where
   getElem a i _ := a.get i
   setElem a i := a.set i
   getElem_setElem_self a i v := a.getElem_set_self i.2
@@ -90,24 +78,22 @@ instance : AssocDArray (Vector.WithDefault α n f) (Fin n) α f where
 
 end Vector.WithDefault
 
-namespace AssocArray
-
-export AssocDArray (getElem_default)
+namespace DefaultDict
 
 class Ext (C : Type*) [Inhabited C] (ι : outParam Type*) (α : outParam Type*)
-    (d : outParam α) [AssocArray C ι α d] : Prop where
+    (d : outParam α) [DefaultDict C ι α fun _ ↦ d] : Prop where
   ext : ∀ {m₁ m₂ : C}, (∀ i : ι, m₁[i] = m₂[i]) → m₁ = m₂
 
-variable {C : Type*} [Inhabited C] {ι : Type*} {α : Type*} {d : α} [AssocArray C ι α d]
+variable {C : Type*} [Inhabited C] {ι : Type*} {α : Type*} {d : α} [DefaultDict C ι α fun _ ↦ d]
 
 variable (C)
 
 protected def Quotient := @Quotient C (Setoid.ker (fun (a : C) (i : ι) ↦ a[i]))
 
-instance : Inhabited (AssocArray.Quotient C) :=
+instance : Inhabited (DefaultDict.Quotient C) :=
   inferInstanceAs <| Inhabited (@Quotient C (Setoid.ker _))
 
-instance : AssocArray (AssocArray.Quotient C) ι α d where
+instance : DefaultDict (DefaultDict.Quotient C) ι α fun _ ↦ d where
   getElem c i _ := Quotient.lift (·[·] : C → ι → α) (fun _ _ ↦ id) c i
   setElem q i v := q.map' (·[i ↦ v]) fun _ _ hm ↦ funext fun j ↦ by
     classical simp [congrFun hm j]
@@ -120,7 +106,7 @@ instance : AssocArray (AssocArray.Quotient C) ι α d where
     induction a using Quotient.ind
     exact coe_toDFinsupp'_eq_getElem _
 
-instance : Ext (AssocArray.Quotient C) ι α d where
+instance : Ext (DefaultDict.Quotient C) ι α d where
   ext {m₁ m₂} := m₂.inductionOn <| m₁.inductionOn (fun _ _ ha ↦ Quotient.sound <| funext ha)
 export Ext (ext)
 
@@ -171,18 +157,17 @@ abbrev toOfFn [Fintype ι] (f : ι → α) : OfFn C ι α f where
     convert (getElem_indicator _ _ _).trans <| dif_pos <| Finset.mem_univ _
     classical infer_instance
 
-end AssocArray
+end DefaultDict
 
-class HasDefaultAssocDArray (ι : Type u) (α : Type v) (f : ι → α)
-    (DefaultAssocDArray : outParam <| Type max u v)
-    [Inhabited DefaultAssocDArray] where
-  [toAssocDArray : AssocDArray DefaultAssocDArray ι α f]
+class HasDefaultDict (ι : Type*) (α : Type*) (f : ι → α) (C : outParam <| Type*)
+    [Inhabited C] where
+  [toDefaultDict : DefaultDict C ι α f]
 
 @[nolint unusedArguments]
-def DefaultAssocDArray (ι : Type u) (α : Type v) (f : ι → α) {D : Type _} [Inhabited D]
-    [HasDefaultAssocDArray ι α f D] :=
-  D
+def mkDefaultDict (ι : Type*) (α : Type*) (f : ι → α) {D : Type*} [Inhabited D]
+    [HasDefaultDict ι α f D] : D :=
+  default
 
-instance {n α f} : HasDefaultAssocDArray (Fin n) α f (Vector.WithDefault α n f) where
+instance {n α f} : HasDefaultDict (Fin n) α f (Vector.WithDefault α n f) where
 
-example {n α f} := DefaultAssocDArray (Fin n) α f
+example {n α f} := mkDefaultDict (Fin n) α f
diff --git a/Algorithm/Data/Classes/Dict.lean b/Algorithm/Data/Classes/Dict.lean
index c52b872..6bf07cb 100644
--- a/Algorithm/Data/Classes/Dict.lean
+++ b/Algorithm/Data/Classes/Dict.lean
@@ -3,8 +3,8 @@ Copyright (c) 2024 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-import Algorithm.Data.Classes.AssocArray
 import Algorithm.Data.Classes.Bag
+import Algorithm.Data.Classes.DefaultDict
 import Algorithm.Data.Classes.GetElem
 
 variable {C ι α : Type*}
@@ -29,20 +29,20 @@ instance : Inhabited C where
 instance : LawfulErase C ι := lawfulErase_iff_toFinset.mpr fun c i ↦ by
   ext; simp [valid_erase, eq_comm]
 
-def Dict.AssocArray (C : Type*) := C
+def Dict.DefaultDict (C : Type*) := C
 
-def Dict.toAssocArray : C ≃ Dict.AssocArray C := Equiv.refl _
+def Dict.toDefaultDict : C ≃ Dict.DefaultDict C := Equiv.refl _
 
-instance : Inhabited (Dict.AssocArray C) where
-  default := Dict.toAssocArray ∅
+instance : Inhabited (Dict.DefaultDict C) where
+  default := Dict.toDefaultDict ∅
 
-instance [Dict C ι α] : AssocArray (Dict.AssocArray C) ι (Option α) none where
-  getElem a i _ := (Dict.toAssocArray.symm a)[i]?
-  toDFinsupp' a := .mk' ((Dict.toAssocArray.symm a)[·]?)
-    (.mk ⟨toMultiset (Dict.toAssocArray.symm a), fun i ↦ by
+instance [Dict C ι α] : DefaultDict (Dict.DefaultDict C) ι (Option α) fun _ ↦ none where
+  getElem a i _ := (Dict.toDefaultDict.symm a)[i]?
+  toDFinsupp' a := .mk' ((Dict.toDefaultDict.symm a)[·]?)
+    (.mk ⟨toMultiset (Dict.toDefaultDict.symm a), fun i ↦ by
       simp [mem_toMultiset, or_iff_not_imp_left] ⟩)
   coe_toDFinsupp'_eq_getElem := by simp
-  setElem c i x := Dict.toAssocArray <| alterElem (Dict.toAssocArray.symm c) i (fun _ ↦ x)
+  setElem c i x := Dict.toDefaultDict <| alterElem (Dict.toDefaultDict.symm c) i (fun _ ↦ x)
   getElem_setElem_self := by simp
   getElem_setElem_of_ne _ _ _ _ hij := by simp [hij]
   getElem_default _ := by simpa [default] using getElem?_neg (cont := C) _ _ (not_mem_empty _)
diff --git a/Algorithm/Data/Classes/IndexedMinHeap.lean b/Algorithm/Data/Classes/IndexedMinHeap.lean
index 985af08..85b327f 100644
--- a/Algorithm/Data/Classes/IndexedMinHeap.lean
+++ b/Algorithm/Data/Classes/IndexedMinHeap.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-import Algorithm.Data.Classes.AssocArray
+import Algorithm.Data.Classes.DefaultDict
 import Algorithm.Data.Classes.MinHeap
 import Algorithm.Data.Classes.ToList
 import Mathlib.Data.Finset.Lattice.Fold
@@ -11,7 +11,7 @@ import Mathlib.Data.Prod.Lex
 
 class IndexedMinHeap (C : Type*) [Inhabited C] (ι : outParam Type*)
     (α : outParam Type*) [Preorder α] [IsTotal α (· ≤ ·)] [OrderTop α] extends
-    AssocDArray C ι α fun _ ↦ ⊤ where
+    DefaultDict C ι α fun _ ↦ ⊤ where
   minIdx : C → ι
   getElem_minIdx_le c (i : ι) : c[minIdx c] ≤ c[i]
   decreaseKey (c : C) (i : ι) : ∀ v < c[i], C := fun v _ ↦ c[i ↦ v]
@@ -63,7 +63,7 @@ variable {α : Type*} [LinearOrder α] {n : ℕ} [NeZero n] {d : Fin n → α}
 
 section ReadOnly
 
-variable [AssocDArray.ReadOnly (Vector α n) (Fin n) α d]
+variable [DefaultDict.ReadOnly (Vector α n) (Fin n) α d]
 
 abbrev minAux (a : Vector α n) : Lex (α × Fin n) :=
   (⊤ : Finset (Fin n)).inf' ⟨0, Finset.mem_univ 0⟩ (fun i ↦ toLex (a[i], i))
@@ -107,17 +107,17 @@ instance (α) (x : WithTop α) : Decidable (x = ⊤) :=
 
 end WithTop
 
-structure AssocArrayWithHeap.WithIdx (α ι : Type*) where
+structure DefaultDictWithHeap.WithIdx (α ι : Type*) where
   val : α
   idx : ι
 
-namespace AssocArrayWithHeap.WithIdx
+namespace DefaultDictWithHeap.WithIdx
 variable {α ι : Type*}
 
-instance [LE α] : LE (AssocArrayWithHeap.WithIdx α ι) where
+instance [LE α] : LE (DefaultDictWithHeap.WithIdx α ι) where
   le x y := x.val ≤ y.val
 
-lemma le_def [LE α] {x y : AssocArrayWithHeap.WithIdx α ι} :
+lemma le_def [LE α] {x y : DefaultDictWithHeap.WithIdx α ι} :
     x ≤ y ↔ x.val ≤ y.val :=
   Iff.rfl
 
@@ -126,7 +126,7 @@ lemma mk_le_mk [LE α] {x y : α} {xi yi : ι} :
     mk x xi ≤ mk y yi ↔ x ≤ y :=
   Iff.rfl
 
-instance [LT α] : LT (AssocArrayWithHeap.WithIdx α ι) where
+instance [LT α] : LT (DefaultDictWithHeap.WithIdx α ι) where
   lt x y := x.val < y.val
 
 @[simp]
@@ -134,65 +134,65 @@ lemma mk_lt_mk [LT α] {x y : α} {xi yi : ι} :
     mk x xi < mk y yi ↔ x < y :=
   Iff.rfl
 
-instance [Preorder α] : Preorder (AssocArrayWithHeap.WithIdx α ι) where
+instance [Preorder α] : Preorder (DefaultDictWithHeap.WithIdx α ι) where
   le_refl _ := le_refl _
   le_trans _ _ _ := le_trans
   lt_iff_le_not_ge _ _ := lt_iff_le_not_ge
 
 instance [Preorder α] [IsTotal α (· ≤ ·)] :
-    IsTotal (AssocArrayWithHeap.WithIdx α ι) (· ≤ ·) where
+    IsTotal (DefaultDictWithHeap.WithIdx α ι) (· ≤ ·) where
   total _ _ := total_of (α := α) (· ≤ ·) _ _
 
-end AssocArrayWithHeap.WithIdx
+end DefaultDictWithHeap.WithIdx
 
-structure AssocArrayWithHeap (C C' : Type*) {ι α : Type*} [Preorder α] [IsTotal α (· ≤ ·)]
-    [Inhabited C] [AssocArray C ι (WithTop α) ⊤]
-    [MinHeap C' (AssocArrayWithHeap.WithIdx α ι)] where mk' ::
-  assocArray : C
+structure DefaultDictWithHeap (C C' : Type*) {ι α : Type*} [Preorder α] [IsTotal α (· ≤ ·)]
+    [Inhabited C] [DefaultDict C ι (WithTop α) ⊤]
+    [MinHeap C' (DefaultDictWithHeap.WithIdx α ι)] where mk' ::
+  defaultDict : C
   minHeap : C'
-  mem_minHeap' : ∀ i : ι, (hi : assocArray[i] ≠ ⊤) → ⟨assocArray[i].untop hi, i⟩ ∈ minHeap
+  mem_minHeap' : ∀ i : ι, (hi : defaultDict[i] ≠ ⊤) → ⟨defaultDict[i].untop hi, i⟩ ∈ minHeap
   getElem_minIdx' : (h : ¬isEmpty minHeap) →
-    assocArray[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val
+    defaultDict[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val
 
-namespace AssocArrayWithHeap
+namespace DefaultDictWithHeap
 variable {C C' : Type*} {ι α : Type*} [Preorder α] [IsTotal α (· ≤ ·)]
-  [Inhabited C] [AssocArray C ι (WithTop α) ⊤]
-  [MinHeap C' (AssocArrayWithHeap.WithIdx α ι)]
+  [Inhabited C] [DefaultDict C ι (WithTop α) ⊤]
+  [MinHeap C' (DefaultDictWithHeap.WithIdx α ι)]
 
-instance : AssocArray.ReadOnly (AssocArrayWithHeap C C') ι (WithTop α) ⊤ where
-  getElem c i _ := c.assocArray[i]
-  toDFinsupp' c := toDFinsupp' c.assocArray
-  coe_toDFinsupp'_eq_getElem c := coe_toDFinsupp'_eq_getElem c.assocArray
+instance : DefaultDict.ReadOnly (DefaultDictWithHeap C C') ι (WithTop α) ⊤ where
+  getElem c i _ := c.defaultDict[i]
+  toDFinsupp' c := toDFinsupp' c.defaultDict
+  coe_toDFinsupp'_eq_getElem c := coe_toDFinsupp'_eq_getElem c.defaultDict
 
 @[simp]
-lemma assocArray_getElem (c : AssocArrayWithHeap C C') (i : ι) :
-    c.assocArray[i] = c[i] :=
+lemma defaultDict_getElem (c : DefaultDictWithHeap C C') (i : ι) :
+    c.defaultDict[i] = c[i] :=
   rfl
 
-lemma mem_minHeap (c : AssocArrayWithHeap C C') :
+lemma mem_minHeap (c : DefaultDictWithHeap C C') :
     ∀ i : ι, (hi : c[i] ≠ ⊤) → ⟨c[i].untop hi, i⟩ ∈ c.minHeap :=
   c.mem_minHeap'
 
-lemma getElem_minIdx (c : AssocArrayWithHeap C C') (h : ¬isEmpty c.minHeap) :
+lemma getElem_minIdx (c : DefaultDictWithHeap C C') (h : ¬isEmpty c.minHeap) :
     c[(MinHeap.head c.minHeap h).idx] = (MinHeap.head c.minHeap h).val :=
   c.getElem_minIdx' h
 
-instance : Inhabited (AssocArrayWithHeap C C') where
+instance : Inhabited (DefaultDictWithHeap C C') where
   default := ⟨default, ∅, by simp, by simp [sizeTM_eq_card_toMultiset, isEmpty_iff_sizeTM_eq_zero]⟩
 
-def mk [DecidableEq α] (assocArray : C) (minHeap : C')
-    (mem_minHeap : ∀ i : ι, (hi : assocArray[i] ≠ ⊤) → ⟨(assocArray[i]).untop hi, i⟩ ∈ minHeap) :
-    AssocArrayWithHeap C C' :=
+def mk [DecidableEq α] (defaultDict : C) (minHeap : C')
+    (mem_minHeap : ∀ i : ι, (hi : defaultDict[i] ≠ ⊤) → ⟨(defaultDict[i]).untop hi, i⟩ ∈ minHeap) :
+    DefaultDictWithHeap C C' :=
   if h : isEmpty minHeap then
-    ⟨assocArray, minHeap, mem_minHeap, (False.elim <| · h)⟩
-  else if h' : assocArray[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val then
-    ⟨assocArray, minHeap, mem_minHeap, fun _ ↦ h'⟩
+    ⟨defaultDict, minHeap, mem_minHeap, (False.elim <| · h)⟩
+  else if h' : defaultDict[(MinHeap.head minHeap h).idx] = (MinHeap.head minHeap h).val then
+    ⟨defaultDict, minHeap, mem_minHeap, fun _ ↦ h'⟩
   else
     haveI : DecidableEq (WithIdx α ι) := by classical infer_instance
     have : sizeTM (MinHeap.tail minHeap) < sizeTM minHeap := by
       simpa [h, sizeTM_eq_card_toMultiset, Multiset.card_erase_lt_of_mem] using
         Multiset.card_erase_lt_of_mem (MinHeap.head_mem_toMultiset _ _)
-    mk assocArray (MinHeap.tail minHeap) fun i hi ↦ by
+    mk defaultDict (MinHeap.tail minHeap) fun i hi ↦ by
       simp only [← mem_toMultiset, MinHeap.toMultiset_tail, h, Bool.false_eq_true, ↓reduceDIte,
         MinHeap.head_def]
       rw [Multiset.mem_erase_of_ne, mem_toMultiset]
@@ -203,33 +203,33 @@ def mk [DecidableEq α] (assocArray : C) (minHeap : C')
 termination_by sizeTM minHeap
 
 @[simp, nolint unusedHavesSuffices] -- false positive
-lemma mk_assocArray [DecidableEq α] (assocArray : C) (minHeap : C')
-    (mem_minHeap : ∀ i : ι, (hi : assocArray[i] ≠ ⊤) → ⟨(assocArray[i]).untop hi, i⟩ ∈ minHeap) :
-    (mk assocArray minHeap mem_minHeap).assocArray = assocArray := by
+lemma mk_defaultDict [DecidableEq α] (defaultDict : C) (minHeap : C')
+    (mem_minHeap : ∀ i : ι, (hi : defaultDict[i] ≠ ⊤) → ⟨(defaultDict[i]).untop hi, i⟩ ∈ minHeap) :
+    (mk defaultDict minHeap mem_minHeap).defaultDict = defaultDict := by
   induction minHeap, mem_minHeap using mk.induct
   all_goals unfold mk; simp [*]
 
 @[simp]
-lemma default_assocArray :
-    (default : AssocArrayWithHeap C C').assocArray = default :=
+lemma default_defaultDict :
+    (default : DefaultDictWithHeap C C').defaultDict = default :=
   rfl
 
 @[simp]
 lemma default_minHeap :
-    (default : AssocArrayWithHeap C C').minHeap = ∅ :=
+    (default : DefaultDictWithHeap C C').minHeap = ∅ :=
   rfl
 
 instance [DecidableEq α] :
-    AssocArray (AssocArrayWithHeap C C') ι (WithTop α) ⊤ where
+    DefaultDict (DefaultDictWithHeap C C') ι (WithTop α) ⊤ where
   setElem c i x :=
     mk
-      c.assocArray[i ↦ x]
+      c.defaultDict[i ↦ x]
       (if hx : x = ⊤ then c.minHeap else insert ⟨x.untop hx, i⟩ c.minHeap)
       fun j hj ↦ by
         haveI : DecidableEq ι := by classical infer_instance
         split_ifs with hx <;>
           simp? [Function.update_apply] at hj ⊢ says
-            simp only [all_valid, getElem_setElem, assocArray_getElem, ne_eq] at hj ⊢
+            simp only [all_valid, getElem_setElem, defaultDict_getElem, ne_eq] at hj ⊢
         · subst hx
           rw [ite_eq_left_iff, Classical.not_imp] at hj
           simp only [hj.1, ↓reduceIte]
@@ -244,12 +244,12 @@ instance [DecidableEq α] :
   getElem_default := by simp [getElem]
 
 @[simp]
-lemma set_assocArray [DecidableEq α] (c : AssocArrayWithHeap C C') (i : ι) (x) :
-    c[i ↦ x].assocArray = c.assocArray[i ↦ x] := by
+lemma set_defaultDict [DecidableEq α] (c : DefaultDictWithHeap C C') (i : ι) (x) :
+    c[i ↦ x].defaultDict = c.defaultDict[i ↦ x] := by
   unfold_projs; simp
 
 instance [Inhabited ι] [DecidableEq α] :
-    IndexedMinHeap (AssocArrayWithHeap C C') ι (WithTop α) where
+    IndexedMinHeap (DefaultDictWithHeap C C') ι (WithTop α) where
   minIdx c := if h : isEmpty c.minHeap then default else (MinHeap.head c.minHeap h).idx
   getElem_minIdx_le c i := by
     split_ifs with h
@@ -263,4 +263,4 @@ instance [Inhabited ι] [DecidableEq α] :
       refine (WithIdx.le_def.mp <| MinHeap.head_le c.minHeap _ (c.mem_minHeap i ?_)).trans ?_ <;>
         simp [hx]
 
-end AssocArrayWithHeap
+end DefaultDictWithHeap
diff --git a/Algorithm/Data/Graph/AdjList.lean b/Algorithm/Data/Graph/AdjList.lean
index 265673a..3e12e6f 100644
--- a/Algorithm/Data/Graph/AdjList.lean
+++ b/Algorithm/Data/Graph/AdjList.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuyang Zhao
 -/
-import Algorithm.Data.Classes.AssocArray
+import Algorithm.Data.Classes.DefaultDict
 import Algorithm.Data.Classes.ToList
 -- import Mathlib.Data.List.Nodup
 import Mathlib.Combinatorics.Quiver.Path
@@ -12,7 +12,7 @@ structure AdjList
     (V : Type*) (Info : Type*)
     (EColl : Type*) [ToMultiset EColl Info] [EmptyCollection EColl]
     [LawfulEmptyCollection EColl Info]
-    (StarColl : Type*) [AssocArray.ReadOnly StarColl V EColl ∅] where
+    (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] where
   protected snd : Info → V
   protected star : StarColl
 
@@ -20,7 +20,7 @@ structure AdjList₂
     (V : Type*) (Info : Type*)
     (EColl : Type*) [ToMultiset EColl Info] [EmptyCollection EColl]
     [LawfulEmptyCollection EColl Info]
-    (StarColl : Type*) [AssocArray.ReadOnly StarColl V EColl ∅] extends
+    (StarColl : Type*) [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] extends
     AdjList V Info EColl StarColl where
   fst : Info → V
   costar : StarColl
@@ -36,7 +36,7 @@ class AdjListClass (G : Type*)
     (V : outParam <| Type*) (Info : outParam <| Type*)
     (EColl : outParam <| Type*) [ToMultiset EColl Info] [EmptyCollection EColl]
     [LawfulEmptyCollection EColl Info]
-    (StarColl : outParam <| Type*) [AssocArray.ReadOnly StarColl V EColl ∅] where
+    (StarColl : outParam <| Type*) [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅] where
   snd : G → Info → V
   star : G → StarColl
 
@@ -56,7 +56,7 @@ variable
   {V : Type*} {Info : Type*}
   {EColl : Type*} [ToMultiset EColl Info] [EmptyCollection EColl]
   [LawfulEmptyCollection EColl Info]
-  {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅]
+  {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅]
 
 instance : AdjListClass (AdjList V Info EColl StarColl) V Info EColl StarColl where
   snd := AdjList.snd
@@ -365,7 +365,7 @@ variable
   {V : Type*} {Info : Type*}
   {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl]
   [LawfulEmptyCollection EColl Info]
-  {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅]
+  {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅]
   {G : Type*} [AdjListClass G V Info EColl StarColl] (g : G)
 
 def succList (v : V) : List V := (toList g[v]).map g..snd
diff --git a/Algorithm/Data/Graph/IsDFSForest.lean b/Algorithm/Data/Graph/IsDFSForest.lean
index 9f2be51..ae471f3 100644
--- a/Algorithm/Data/Graph/IsDFSForest.lean
+++ b/Algorithm/Data/Graph/IsDFSForest.lean
@@ -14,7 +14,7 @@ variable
   {V : Type*} {Info : Type*}
   {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl]
   [LawfulEmptyCollection EColl Info]
-  {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅]
+  {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅]
   {G : Type*} [AdjListClass G V Info EColl StarColl] {g : G}
 
 variable (g) in
diff --git a/Algorithm/Data/UnionFind.lean b/Algorithm/Data/UnionFind.lean
index 0b1dbfe..6bac679 100644
--- a/Algorithm/Data/UnionFind.lean
+++ b/Algorithm/Data/UnionFind.lean
@@ -173,7 +173,7 @@ lemma find_snd_root (self : UnionFind ι P S) (i : ι) :
   rootCore_findAux_snd self.parent self.wf i _
 
 omit [DecidableEq ι] in
-lemma wellFounded_assocArraySet (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k])
+lemma wellFounded_defaultDictSet (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k])
     (i r : ι) (hr : parent[r] = r) :
     WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[i ↦ r][k] := by
   refine ⟨fun x ↦ ?_⟩
@@ -193,7 +193,7 @@ set_option linter.unusedVariables false in -- easier to `rw` and `simp`
 def setParent (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦ i ≠ j ∧ i = parent[j])
     (i j : ι) (hi : parent[i] = i) (hj : parent[j] = j) (s : ℕ) :
     UnionFind ι P S :=
-  ⟨parent[i ↦ j], size[j ↦ s], wellFounded_assocArraySet parent wf i j hj⟩
+  ⟨parent[i ↦ j], size[j ↦ s], wellFounded_defaultDictSet parent wf i j hj⟩
 
 @[simp]
 lemma setParent_parent_eq_parent (parent : P) (size : S)
diff --git a/Algorithm/Graph/DFS.lean b/Algorithm/Graph/DFS.lean
index 63dea3a..734deb2 100644
--- a/Algorithm/Graph/DFS.lean
+++ b/Algorithm/Graph/DFS.lean
@@ -12,7 +12,7 @@ namespace AdjListClass
 variable {V : Type*} {Info : Type*}
   {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl]
   [LawfulEmptyCollection EColl Info]
-  {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅]
+  {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅]
   {G : Type*} [AdjListClass G V Info EColl StarColl]
 
 -- 也许在以后可以改成存迭代器
@@ -20,7 +20,7 @@ variable {V : Type*} {Info : Type*}
 
 def dfsForest' (g : G)
     [Fintype V] {BoolArray : Type*}
-    [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+    [Inhabited BoolArray] [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     Forest V × { b : BoolArray // [DecidableEq V] →
       (toDFinsupp' visited).support ⊆ (toDFinsupp' b).support } :=
@@ -55,7 +55,7 @@ decreasing_by
 
 lemma roots_dfsForest'_fst_subset (g : G)
     [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     (g..dfsForest' vs visited).1.roots ⊆ {v | v ∈ vs} := by
   match vs with
@@ -72,7 +72,7 @@ lemma roots_dfsForest'_fst_subset (g : G)
 
 lemma subset_support_toDFinsupp'_dfsForest'_snd (g : G)
     [DecidableEq V] [Fintype V] {BoolArray : Type*}
-    [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+    [Inhabited BoolArray] [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     {v | v ∈ vs} ⊆ (toDFinsupp' (g..dfsForest' vs visited).2.val).support := by
   match vs with
@@ -93,7 +93,7 @@ lemma subset_support_toDFinsupp'_dfsForest'_snd (g : G)
 
 lemma isDFSForest_dfsForest' (g : G)
     [DecidableEq V] [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     g..IsDFSForest
       (toDFinsupp' visited).support
@@ -116,14 +116,14 @@ lemma isDFSForest_dfsForest' (g : G)
 
 def dfsForest (g : G)
     [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     Forest V × BoolArray :=
   (g..dfsForest' vs visited).map id Subtype.val
 
 lemma dfsForest_spec' (g : G)
     [Fintype V] (BoolArray : Type*) [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false] (vs : List V) :
+    [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) :
     let (f, vis) := (g..dfsForest vs (default : BoolArray))
     ([DecidableEq V] → f.support = (toDFinsupp' vis).support) ∧
       ∀ v, v ∈ f.support ↔ ∃ r ∈ vs, g..Reachable r v := by
@@ -139,7 +139,7 @@ lemma dfsForest_spec' (g : G)
 
 lemma dfsForest_spec (g : G)
     [Fintype V] (BoolArray : Type*) [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false] (vs : List V) :
+    [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) :
     let (f, vis) := (g..dfsForest vs (default : BoolArray))
     f.support = {v : V | vis[v]} ∧ ∀ v : V, vis[v] ↔ ∃ r ∈ vs, g..Reachable r v := by
   letI : Unique (DecidableEq V) := uniqueOfSubsingleton <| by classical infer_instance
@@ -150,8 +150,8 @@ lemma dfsForest_spec (g : G)
   · ext; simp
   · simp [H.1]
 
-def dfs' (g : G)
-    [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+def dfs' (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     { b : BoolArray // ([DecidableEq V] →
       (toDFinsupp' visited).support ⊆ (toDFinsupp' b).support) ∧
@@ -186,8 +186,8 @@ decreasing_by
       simpa using h.trans h₁
     simpa [Prod.lex_iff, ← le_iff_lt_or_eq] using this
 
-def dfs (g : G)
-    [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+def dfs (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     BoolArray :=
   (g..dfs' vs visited).val
@@ -195,20 +195,20 @@ def dfs (g : G)
 @[simp]
 lemma dfsForest_snd (g : G)
     [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     (g..dfsForest vs visited).snd = g..dfs vs visited :=
   (g..dfs' vs visited).prop.2.symm
 
 lemma dfs_spec (g : G)
     [Fintype V] (BoolArray : Type*) [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false] (vs : List V) :
+    [DefaultDict BoolArray V Bool fun _ ↦ false] (vs : List V) :
     ∀ v : V, (g..dfs vs (default : BoolArray))[v] ↔ ∃ r ∈ vs, g..Reachable r v :=
   g..dfsForest_snd vs (default : BoolArray) ▸ (g..dfsForest_spec BoolArray vs).2
 
 def dfsForestTR (g : G)
     [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List (Forest V × List V)) (visited : BoolArray) :
     Forest V × BoolArray :=
   match vs with
@@ -237,8 +237,8 @@ decreasing_by
     rw [Finset.subset_iff]
     simp [*, Function.update]
 
-def dfs'TR (g : G)
-    [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+def dfs'TR (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List (List V)) (visited : BoolArray) :
     BoolArray :=
   match vs with
@@ -264,8 +264,8 @@ decreasing_by
     rw [Finset.subset_iff]
     simp [*, Function.update]
 
-def dfsTR (g : G)
-    [Fintype V] {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+def dfsTR (g : G) [Fintype V] {BoolArray : Type*} [Inhabited BoolArray]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     BoolArray :=
   match vs with
@@ -290,7 +290,7 @@ decreasing_by
 
 lemma dfsTR_spec' (g : G)
     [Fintype V] [DecidableEq V]
-    {BoolArray : Type*} [Inhabited BoolArray] [AssocArray BoolArray V Bool false]
+    {BoolArray : Type*} [Inhabited BoolArray] [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) (visited : BoolArray) :
     g..traversal (toDFinsupp' visited).support {v | v ∈ vs ∧ v ∉ (toDFinsupp' visited).support} =
       g..traversal (toDFinsupp' (g..dfsTR vs visited)).support ∅ := by
@@ -316,7 +316,7 @@ lemma dfsTR_spec' (g : G)
 
 lemma dfsTR_spec (g : G)
     [Fintype V] (BoolArray : Type*) [Inhabited BoolArray]
-    [AssocArray BoolArray V Bool false]
+    [DefaultDict BoolArray V Bool fun _ ↦ false]
     (vs : List V) :
     g..traversal ∅ {v | v ∈ vs} = {v : V | (g..dfsTR vs (default : BoolArray))[v]} := by
   letI : DecidableEq V := by classical infer_instance
diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean
index de968b9..a07065c 100644
--- a/Algorithm/Graph/Dijkstra.lean
+++ b/Algorithm/Graph/Dijkstra.lean
@@ -104,7 +104,7 @@ namespace AdjListClass
 variable {V : Type*} {Info : Type*}
   {EColl : Type*} [ToList EColl Info] [EmptyCollection EColl]
   [LawfulEmptyCollection EColl Info]
-  {StarColl : Type*} [AssocArray.ReadOnly StarColl V EColl ∅]
+  {StarColl : Type*} [DefaultDict.ReadOnly StarColl V EColl fun _ ↦ ∅]
   {G : Type*} [AdjListClass G V Info EColl StarColl]
   {CostType : Type*}
 
@@ -373,7 +373,7 @@ lemma isDist_union {g : G}
 
 def dijkstraStep (g : G) (c : Info → CostType)
     [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray)
     (hMinIdx : heap[minIdx heap] ≠ ⊤) :
@@ -388,7 +388,7 @@ def dijkstraStep (g : G) (c : Info → CostType)
 
 structure dijkstraStep.Spec (g : G) (c : Info → CostType)
     [AddMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (init : DistHeap) (heap : DistHeap) (res : DistArray) : Prop where
   h₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤
@@ -402,7 +402,7 @@ structure dijkstraStep.Spec (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_snd_getElem (g : G) (c : Info → CostType)
     [DecidableEq V] [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) :
     (dijkstraStep g c heap res hMinIdx).2[v] =
@@ -411,7 +411,7 @@ lemma dijkstraStep_snd_getElem (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType)
     [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) :
     (dijkstraStep g c heap res hMinIdx).2[v] = ⊤ ↔
@@ -424,7 +424,7 @@ lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_snd_support (g : G) (c : Info → CostType)
     [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) :
     {v : V | (dijkstraStep g c heap res hMinIdx).2[v] ≠ ⊤} =
@@ -435,7 +435,7 @@ lemma dijkstraStep_snd_support (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType)
     [DecidableEq V] [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤)
     (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) :
@@ -473,7 +473,7 @@ lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType)
 lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType)
     [DecidableEq V] [DecidableEq Info]
     [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤)
     (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) :
@@ -499,7 +499,7 @@ lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType)
     [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤)
     (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) :
@@ -522,7 +522,7 @@ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_fst_support (g : G) (c : Info → CostType)
     [AddCommMonoid CostType] [LinearOrder CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤)
     (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) :
@@ -537,7 +537,7 @@ lemma dijkstraStep_fst_support (g : G) (c : Info → CostType)
 
 lemma dijkstraStep_spec (g : G) (c : Info → CostType)
     [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType]
-    {DistArray : Type*} [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    {DistArray : Type*} [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (init : DistHeap) (heap : DistHeap) (res : DistArray)
     (h : dijkstraStep.Spec g c init heap res) (hMinIdx : heap[minIdx heap] ≠ ⊤) :
@@ -680,7 +680,7 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType)
 
 def dijkstra (g : G) (c : Info → CostType)
     [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType]
-    (DistArray : Type*) [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (init : DistHeap) :
     DistArray :=
@@ -704,7 +704,7 @@ termination_by Fintype.card {v : V | res[v] = ⊤}
   spec_init : dijkstraStep.Spec g c init init default := by
     constructor
     · simp
-    · simp only [AssocDArray.getElem_default, ne_eq,
+    · simp only [DefaultDict.getElem_default, ne_eq,
         not_true_eq_false, IsEmpty.forall_iff, implies_true, and_true, Set.mem_setOf_eq,
         forall_true_left]
       intro h
@@ -715,7 +715,7 @@ termination_by Fintype.card {v : V | res[v] = ⊤}
 
 lemma dijkstra_spec (g : G) (c : Info → CostType)
     [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType]
-    (DistArray : Type*) [Inhabited DistArray] [AssocArray DistArray V (WithTop CostType) ⊤]
+    (DistArray : Type*) [Inhabited DistArray] [DefaultDict DistArray V (WithTop CostType) fun _ ↦ ⊤]
     {DistHeap : Type*} [Inhabited DistHeap] [IndexedMinHeap DistHeap V (WithTop CostType)]
     (init : DistHeap) (v : V) :
     g..IsDist c {s | init[s] ≠ ⊤} (fun s hs ↦ init[s].untop hs) v
diff --git a/scripts/nolints.json b/scripts/nolints.json
index 4119c1a..22297a4 100644
--- a/scripts/nolints.json
+++ b/scripts/nolints.json
@@ -1,11 +1,10 @@
 [["docBlame", "AdjList"],
  ["docBlame", "AdjListClass"],
  ["docBlame", "AdjList₂"],
- ["docBlame", "AssocArrayWithHeap"],
  ["docBlame", "Back"],
  ["docBlame", "Bag"],
  ["docBlame", "DecidableMem"],
- ["docBlame", "DefaultAssocDArray"],
+ ["docBlame", "DefaultDictWithHeap"],
  ["docBlame", "Dict"],
  ["docBlame", "Erase"],
  ["docBlame", "Forest"],
@@ -15,7 +14,7 @@
  ["docBlame", "GetSetElemAllValid"],
  ["docBlame", "GetSetEraseElem"],
  ["docBlame", "GetSetEraseElem?"],
- ["docBlame", "HasDefaultAssocDArray"],
+ ["docBlame", "HasDefaultDict"],
  ["docBlame", "HasValid"],
  ["docBlame", "IndexedMinHeap"],
  ["docBlame", "LawfulAppend"],
@@ -39,6 +38,7 @@
  ["docBlame", "alterElem"],
  ["docBlame", "decreaseKeyD"],
  ["docBlame", "decreaseKeysD"],
+ ["docBlame", "mkDefaultDict"],
  ["docBlame", "modifyElem"],
  ["docBlame", "«term__[_=>_]»"],
  ["docBlame", "«term__[_↦_]»"],
@@ -75,24 +75,23 @@
  ["docBlame", "AdjListClass.traversal"],
  ["docBlame", "AdjList₂.costar"],
  ["docBlame", "AdjList₂.fst"],
- ["docBlame", "AssocArray.Ext"],
- ["docBlame", "AssocArray.Quotient"],
- ["docBlame", "AssocArray.ReadOnly"],
- ["docBlame", "AssocArray.indicator"],
- ["docBlame", "AssocArray.listIndicator"],
- ["docBlame", "AssocArray.toOfFn"],
- ["docBlame", "AssocArrayWithHeap.WithIdx"],
- ["docBlame", "AssocArrayWithHeap.assocArray"],
- ["docBlame", "AssocArrayWithHeap.minHeap"],
- ["docBlame", "AssocArrayWithHeap.mk"],
- ["docBlame", "AssocDArray.ReadOnly"],
  ["docBlame", "Back.back"],
  ["docBlame", "Back.back?"],
  ["docBlame", "Back.backD"],
  ["docBlame", "Bag.ReadOnly"],
- ["docBlame", "Dict.AssocArray"],
+ ["docBlame", "DefaultDict.Ext"],
+ ["docBlame", "DefaultDict.Quotient"],
+ ["docBlame", "DefaultDict.ReadOnly"],
+ ["docBlame", "DefaultDict.indicator"],
+ ["docBlame", "DefaultDict.listIndicator"],
+ ["docBlame", "DefaultDict.toOfFn"],
+ ["docBlame", "DefaultDictWithHeap.WithIdx"],
+ ["docBlame", "DefaultDictWithHeap.defaultDict"],
+ ["docBlame", "DefaultDictWithHeap.minHeap"],
+ ["docBlame", "DefaultDictWithHeap.mk"],
+ ["docBlame", "Dict.DefaultDict"],
  ["docBlame", "Dict.ReadOnly"],
- ["docBlame", "Dict.toAssocArray"],
+ ["docBlame", "Dict.toDefaultDict"],
  ["docBlame", "Erase.erase"],
  ["docBlame", "Forest.append"],
  ["docBlame", "Forest.post"],
@@ -102,7 +101,7 @@
  ["docBlame", "Front.front"],
  ["docBlame", "Front.front?"],
  ["docBlame", "Front.frontD"],
- ["docBlame", "HasDefaultAssocDArray.toAssocDArray"],
+ ["docBlame", "HasDefaultDict.toDefaultDict"],
  ["docBlame", "HasValid.Valid"],
  ["docBlame", "IndexedMinHeap.decreaseKey"],
  ["docBlame", "IndexedMinHeap.minIdx"],
@@ -149,10 +148,10 @@
  ["docBlame", "AdjListClass.Quiver.val"],
  ["docBlame", "AdjListClass.dijkstra.go"],
  ["docBlame", "AdjListClass.dijkstraStep.Spec"],
- ["docBlame", "AssocArrayWithHeap.WithIdx.idx"],
- ["docBlame", "AssocArrayWithHeap.WithIdx.val"],
- ["docBlame", "AssocDArray.ReadOnly.toDFinsupp'"],
  ["docBlame", "Bag.ReadOnly.decidableMem"],
+ ["docBlame", "DefaultDict.ReadOnly.toDFinsupp'"],
+ ["docBlame", "DefaultDictWithHeap.WithIdx.idx"],
+ ["docBlame", "DefaultDictWithHeap.WithIdx.val"],
  ["docBlame", "Membership.IsEmpty.isEmpty"],
  ["docBlame", "MultiBag.ReadOnly.count"],
  ["docBlame", "Quiver.Path.cost"],
diff --git a/test/UnionFind.lean b/test/UnionFind.lean
index a23f4ca..0b9b047 100644
--- a/test/UnionFind.lean
+++ b/test/UnionFind.lean
@@ -1,6 +1,5 @@
 import Algorithm.Data.UnionFind
 
-abbrev Vector := Batteries.Vector
 abbrev UF := UnionFind (Fin 10) (Vector (Fin 10) 10) (Vector Nat 10)
 
 /--