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

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

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

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

@[simp]

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