Documentation

Std.Data.DHashMap.IteratorLemmas

source
@[simp]
theorem Std.DHashMap.Internal.AssocList.step_iter_nil {α : Type u} {β : α → Type v} :
nil.iter.step = ⟨Iterators.IterStep.done, ⋯⟩
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.step_iter_cons {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : AssocList α β} :
(cons k v l).iter.step = ⟨Iterators.IterStep.yield l.iter ⟨k, v⟩, ⋯⟩
source
@[simp]
theorem Std.DHashMap.Internal.AssocList.toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} :
l.iter.toList = l.toList
source
@[simp]
theorem Std.DHashMap.Raw.toList_iter {α : Type u} {β : α → Type v} {m : Raw α β} :
m.iter.toList = m.toList
source
@[simp]
theorem Std.DHashMap.Raw.toListRev_iter {α : Type u} {β : α → Type v} {m : Raw α β} :
m.iter.toListRev = m.toList.reverse
source
@[simp]
theorem Std.DHashMap.Raw.toArray_iter {α : Type u} {β : α → Type v} {m : Raw α β} [BEq α] [Hashable α] (h : m.WF) :
m.iter.toArray = m.toArray
source
@[simp]
theorem Std.DHashMap.Raw.toList_keysIter {α : Type u} {β : α → Type u} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysIter.toList = m.keys
source
@[simp]
theorem Std.DHashMap.Raw.toListRev_keysIter {α : Type u} {β : α → Type u} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysIter.toListRev = m.keys.reverse
source
@[simp]
theorem Std.DHashMap.Raw.toArray_keysIter {α : Type u} {β : α → Type u} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysIter.toArray = m.keysArray
source
@[simp]
theorem Std.DHashMap.Raw.toList_valuesIter_eq_toList_map_snd {α β : Type u} {m : Raw α fun (x : α) => β} :
m.valuesIter.toList = List.map Sigma.snd m.toList
source
@[simp]
theorem Std.DHashMap.Raw.toListRev_valuesIter {α β : Type u} {m : Raw α fun (x : α) => β} :
m.valuesIter.toListRev = (List.map Sigma.snd m.toList).reverse
source
@[simp]
theorem Std.DHashMap.Raw.toArray_valuesIter {α β : Type u} {m : Raw α fun (x : α) => β} :
m.valuesIter.toArray = (List.map Sigma.snd m.toList).toArray
source
@[simp]
theorem Std.DHashMap.toList_iter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : DHashMap α β} :
m.iter.toList = m.toList
source
@[simp]
theorem Std.DHashMap.toListRev_iter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : DHashMap α β} :
m.iter.toListRev = m.toList.reverse
source
@[simp]
theorem Std.DHashMap.toArray_iter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : DHashMap α β} :
m.iter.toArray = m.toArray
source
@[simp]
theorem Std.DHashMap.toList_keysIter {α : Type u} {β : α → Type u} [BEq α] [Hashable α] {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] :
m.keysIter.toList = m.keys
source
@[simp]
theorem Std.DHashMap.toListRev_keysIter {α : Type u} {β : α → Type u} [BEq α] [Hashable α] {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] :
m.keysIter.toListRev = m.keys.reverse
source
@[simp]
theorem Std.DHashMap.toArray_keysIter {α : Type u} {β : α → Type u} [BEq α] [Hashable α] {m : DHashMap α β} [EquivBEq α] [LawfulHashable α] :
m.keysIter.toArray = m.keysArray
source
@[simp]
theorem Std.DHashMap.toList_valuesIter_eq_toList_map_snd {α β : Type u} [BEq α] [Hashable α] {m : DHashMap α fun (x : α) => β} :
m.valuesIter.toList = List.map Sigma.snd m.toList
source
@[simp]
theorem Std.DHashMap.toListRev_valuesIter {α β : Type u} [BEq α] [Hashable α] {m : DHashMap α fun (x : α) => β} :
m.valuesIter.toListRev = (List.map Sigma.snd m.toList).reverse
source
@[simp]
theorem Std.DHashMap.toArray_valuesIter {α β : Type u} [BEq α] [Hashable α] {m : DHashMap α fun (x : α) => β} :
m.valuesIter.toArray = (List.map Sigma.snd m.toList).toArray