structure Trie.Raw (α : Type u_1) (β : Type u_2) [DecidableEq α] [Hashable α] : Type (max u_1 u_2)

• inner : Raw₀ α β
• wf : self.inner.WF

theorem Trie.Raw.ext {α : Type u_1} {β : Type u_2} {inst✝ : DecidableEq α} {inst✝¹ : Hashable α} {x y : Raw α β} (inner : x.inner = y.inner) : x = y

theorem Trie.Raw.ext_iff {α : Type u_1} {β : Type u_2} {inst✝ : DecidableEq α} {inst✝¹ : Hashable α} {x y : Raw α β} : x = y ↔ x.inner = y.inner

@[simp]

instance Trie.Raw.instWFInner {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} : t.inner.WF

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

Equations

• t.val = t.inner.val

def Trie.Raw.mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw α β) : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β

Equations

• t.mp = t.inner.mp

@[simp]

theorem Trie.Raw.val_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {inner : Raw₀ α β} {wf : inner.WF} : { inner := inner, wf := wf }.val = inner.val

@[simp]

theorem Trie.Raw.mp_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {inner : Raw₀ α β} {wf : inner.WF} : { inner := inner, wf := wf }.mp = inner.mp

@[irreducible]

def Trie.Raw.rec' {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw α β → Sort u_3} (motive : (val : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → (wf : (Raw₀.mk val mp).WF) → ((i : α) → (t : Raw α β) → mp.get? i = some t.inner → γ t) → γ { inner := Raw₀.mk val mp, wf := wf }) (t : Raw α β) : γ t

Equations

• Trie.Raw.rec' motive { inner := Trie.Raw₀.mk val mp, wf := wf } = motive val mp wf fun (i : α) (t : Trie.Raw α β) (h₁ : mp.get? i = some t.inner) => Trie.Raw.rec' motive { inner := t.inner, wf := ⋯ }

@[reducible, inline]

abbrev Trie.Raw.ind {α : Type u_3} {β : Type u_4} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw α β → Sort u_5} (motive : (val : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → (wf : (Raw₀.mk val mp).WF) → ((i : α) → (t : Raw α β) → mp.get? i = some t.inner → γ t) → γ { inner := Raw₀.mk val mp, wf := wf }) (t : Raw α β) : γ t

Equations

• @Trie.Raw.ind = @Trie.Raw.rec'

@[simp]

theorem Trie.Raw.rec'_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {γ : Raw α β → Sort u_3} {val : Option β} {mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β} {wf : (Raw₀.mk val mp).WF} {motive : (val : Option β) → (mp : Std.DHashMap.Raw α fun (x : α) => Raw₀ α β) → (wf : (Raw₀.mk val mp).WF) → ((i : α) → (t : Raw α β) → mp.get? i = some t.inner → γ t) → γ { inner := Raw₀.mk val mp, wf := wf }} : rec' motive { inner := Raw₀.mk val mp, wf := wf } = motive val mp wf fun (x : α) (t : Raw α β) (h : mp.get? x = some t.inner) => rec' motive t

def Trie.Raw.empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : Raw α β

Equations

• Trie.Raw.empty = { inner := ∅, wf := ⋯ }

@[instance_reducible]

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

Equations

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

theorem Trie.Raw.empty_def {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : ∅ = { inner := ∅, wf := ⋯ }

@[simp]

theorem Trie.Raw.inner_empty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] : ∅.inner = ∅

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

Equations

• t.depth = Trie.Raw.rec' (fun (x : Option β) (mp : Std.DHashMap.Raw α fun (x : α) => Trie.Raw₀ α β) (wf : (Trie.Raw₀.mk x mp).WF) (f : (i : α) → (t : Trie.Raw α β) → mp.get? i = some t.inner → ℕ) => (fun (x_1 : ℕ → (i : α) → (x : Trie.Raw₀ α β) → mp.get? i = some x → ℕ) => mp.foldWith ⋯ x_1 0) fun (acc : ℕ) (i : α) (x_1 : Trie.Raw₀ α β) (h₂ : mp.get? i = some x_1) => max acc (1 + f i { inner := x_1, wf := ⋯ } h₂)) t

@[simp]

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

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

Equations

• t.get1? k = match h : t.mp.get? k with | none => none | some t' => some { inner := t', wf := ⋯ }

theorem Trie.Raw.get1?_eq_some_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {k : α} {t' : Raw α β} : t.get1? k = some t' ↔ t.mp.get? k = some t'.inner

theorem Trie.Raw.depth_eq_depth_inner {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} : t.depth = t.inner.depth

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

@[simp]

theorem Trie.Raw.depth_mk {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {raw : Raw₀ α β} [wf : raw.WF] : { inner := raw, wf := wf }.depth = raw.depth

@[simp]

theorem Trie.Raw.get?_mp_inner_eq_some_inner_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t' : Raw α β} {k : α} : t.inner.mp.get? k = some t'.inner ↔ t.get1? k = some t'

@[simp]

theorem Trie.Raw.WF.mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} : t.mp.WF

theorem Trie.Raw.get?_mp {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {k : α} : t.mp.get? k = Option.map (fun (x : Raw α β) => x.inner) (t.get1? k)

theorem Trie.Raw.mem_of_get?_eq_some {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {k : α} {x : Raw α β} (h : t.get1? k = some x) : k ∈ t.mp

theorem Trie.Raw.mem_mp_iff_get?_eq_some {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {k : α} : k ∈ t.mp ↔ ∃ (x : Raw α β), t.get1? k = some x

def Trie.Raw.isEmpty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw α β) : Prop

Equations

• t.isEmpty = t.inner.isEmpty

@[instance_reducible]

instance Trie.Raw.instDecidableIsEmpty {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} : Decidable t.isEmpty

Equations

• Trie.Raw.instDecidableIsEmpty = inferInstance

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

Equations

• t.setVal val = { inner := t.inner.setVal val, wf := ⋯ }

@[simp]

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

@[simp]

theorem Trie.Raw.mp_setVal {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {val : Option β} : (t.setVal val).mp = t.mp

def Trie.Raw.erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw α β) (i : α) : Raw α β

Equations

• t.erase1 i = { inner := t.inner.erase1 i, wf := ⋯ }

@[simp]

theorem Trie.Raw.val_erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i : α} : (t.erase1 i).val = t.val

@[simp]

theorem Trie.Raw.mp_erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i : α} : (t.erase1 i).mp = t.mp.erase i

def Trie.Raw.insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] (t : Raw α β) (i : α) (t₁ : Raw α β) : Raw α β

Equations

• t.insert1 i t₁ = { inner := t.inner.insert1 i t₁.inner, wf := ⋯ }

@[simp]

theorem Trie.Raw.val_insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i : α} {t₁ : Raw α β} : (t.insert1 i t₁).val = t.val

theorem Trie.Raw.mp_insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw α β} {i : α} : (t.insert1 i t₁).mp = if t₁.isEmpty then t.mp.erase i else t.mp.insert i t₁.inner

theorem Trie.Raw.get1?_eq_get1?_inner {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i : α} : t.get1? i = match h : t.inner.get1? i with | none => none | some t₁ => some { inner := t₁, wf := ⋯ }

theorem Trie.Raw.get1?_eq_some_iff_inner {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i : α} {t₁ : Raw α β} : t.get1? i = some t₁ ↔ t.inner.get1? i = some t₁.inner

theorem Trie.Raw.get1?_eq_none_iff_inner {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i : α} : t.get1? i = none ↔ t.inner.get1? i = none

theorem Trie.Raw.get1?_erase1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i j : α} : (t.erase1 i).get1? j = if i = j then none else t.get1? j

theorem Trie.Raw.get1?_insert1 {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t : Raw α β} {i j : α} {t₁ : Raw α β} : (t.insert1 i t₁).get1? j = if i = j then if t₁.isEmpty then none else some t₁ else t.get1? j

@[simp]

theorem Trie.Raw.get1?_erase1_eq_some_iff {α : Type u_1} {β : Type u_2} [ha₁ : DecidableEq α] [ha₂ : Hashable α] {t t₁ : Raw α β} {i j : α} : (t.erase1 i).get1? j = some t₁ ↔ i ≠ j ∧ t.get1? j = some t₁