Documentation

Std.Data.HashMap.IteratorLemmas

source
@[simp]
theorem Std.HashMap.Raw.toList_iter {α : Type u} {β : Type v} {m : Raw α β} :
m.iter.toList = m.toList
source
@[simp]
theorem Std.HashMap.Raw.toListRev_iter {α : Type u} {β : Type v} {m : Raw α β} :
m.iter.toListRev = m.toList.reverse
source
@[simp]
theorem Std.HashMap.Raw.toArray_iter {α : Type u} {β : Type v} {m : Raw α β} [BEq α] [Hashable α] (h : m.WF) :
m.iter.toArray = m.toArray
source
@[simp]
theorem Std.HashMap.Raw.toList_keysIter {α β : Type u} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysIter.toList = m.keys
source
@[simp]
theorem Std.HashMap.Raw.toListRev_keysIter {α β : Type u} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysIter.toListRev = m.keys.reverse
source
@[simp]
theorem Std.HashMap.Raw.toArray_keysIter {α β : Type u} {m : Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysIter.toArray = m.keysArray
source
@[simp]
theorem Std.HashMap.Raw.toList_valuesIter_eq_toList_map_snd {α β : Type u} {m : Raw α β} :
m.valuesIter.toList = List.map Prod.snd m.toList
source
@[simp]
theorem Std.HashMap.Raw.toListRev_valuesIter {α β : Type u} {m : Raw α β} :
m.valuesIter.toListRev = (List.map Prod.snd m.toList).reverse
source
@[simp]
theorem Std.HashMap.Raw.toArray_valuesIter {α β : Type u} {m : Raw α β} :
m.valuesIter.toArray = (List.map Prod.snd m.toList).toArray
source
@[simp]
theorem Std.HashMap.toList_iter {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : HashMap α β} :
m.iter.toList = m.toList
source
@[simp]
theorem Std.HashMap.toListRev_iter {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : HashMap α β} :
m.iter.toListRev = m.toList.reverse
source
@[simp]
theorem Std.HashMap.toArray_iter {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : HashMap α β} :
m.iter.toArray = m.toArray
source
@[simp]
theorem Std.HashMap.toList_keysIter {α β : Type u} [BEq α] [Hashable α] {m : HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.keysIter.toList = m.keys
source
@[simp]
theorem Std.HashMap.toListRev_keysIter {α β : Type u} [BEq α] [Hashable α] {m : HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.keysIter.toListRev = m.keys.reverse
source
@[simp]
theorem Std.HashMap.toArray_keysIter {α β : Type u} [BEq α] [Hashable α] {m : HashMap α β} [EquivBEq α] [LawfulHashable α] :
m.keysIter.toArray = m.keysArray
source
@[simp]
theorem Std.HashMap.toList_valuesIter_eq_toList_map_snd {α β : Type u} [BEq α] [Hashable α] {m : HashMap α β} :
m.valuesIter.toList = List.map Prod.snd m.toList
source
@[simp]
theorem Std.HashMap.toListRev_valuesIter {α β : Type u} [BEq α] [Hashable α] {m : HashMap α β} :
m.valuesIter.toListRev = (List.map Prod.snd m.toList).reverse
source
@[simp]
theorem Std.HashMap.toArray_valuesIter {α β : Type u} [BEq α] [Hashable α] {m : HashMap α β} :
m.valuesIter.toArray = (List.map Prod.snd m.toList).toArray