structure Trie (α : Type u_3) (β : Type u_4) [DecidableEq α] [Hashable α] : Type (max u_3 u_4)

• inner : Quotient Raw.Setoid

def Trie.ofRaw {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw α β) : Trie α β

Equations

• Trie.ofRaw t = { inner := ⟦t⟧ }

def Trie.empty {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : Trie α β

Equations

• Trie.empty = Trie.ofRaw ∅

@[instance_reducible]

instance Trie.instEmptyCollection {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : EmptyCollection (Trie α β)

Equations

• Trie.instEmptyCollection = { emptyCollection := Trie.empty }

theorem Trie.empty_def {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : ∅ = empty

def Trie.depth {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Trie α β) : ℕ

Equations

• t.depth = Quotient.lift Trie.Raw.depth ⋯ t.inner

@[simp]

theorem Trie.depth_empty {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : ∅.depth = 0

theorem Trie.option_map_ofRaw_get1?_eq_of_equiv {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {a b : Raw α β} {k : α} (h₁ : a.Equiv b) : Option.map ofRaw (a.get1? k) = Option.map ofRaw (b.get1? k)

def Trie.get1? {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Trie α β) (k : α) : Option (Trie α β)

Equations

• t.get1? k = Quotient.lift (fun (t : Trie.Raw α β) => Option.map Trie.ofRaw (t.get1? k)) ⋯ t.inner

theorem Trie.depth_lt {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t' : Trie α β} {k : α} (h : t.get1? k = some t') : t'.depth < t.depth

def Trie.eqComp {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb : DecidableEq β] (t₁ t₂ : Trie α β) : Bool

Equations

• t₁.eqComp t₂ = t₁.inner.liftOn₂ t₂.inner Trie.Raw.equivComp ⋯

theorem Trie.eq_iff_eqComp {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Trie α β} [hb : DecidableEq β] : t₁ = t₂ ↔ t₁.eqComp t₂ = true

@[instance_reducible]

instance Trie.instDecidableEq {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] [hb : DecidableEq β] : DecidableEq (Trie α β)

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_bool (x✝¹.eqComp x✝) ⋯

@[simp]

theorem Trie.eqComp_iff_decide_eq {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t₁ t₂ : Trie α β} [hb : DecidableEq β] : t₁.eqComp t₂ = true ↔ decide (t₁ = t₂) = true

def Trie.val {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Trie α β) : Option β

Equations

• t.val = Quotient.lift Trie.Raw.val ⋯ t.inner

def Trie.setVal {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Trie α β) (val : Option β) : Trie α β

Equations

• t.setVal val = { inner := Quotient.map (fun (x : Trie.Raw α β) => x.setVal val) ⋯ t.inner }

@[simp]

theorem Trie.val_setVal {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Trie α β} {val : Option β} : (t.setVal val).val = val