Documentation

Std.Data.HashSet.IteratorLemmas

source
@[simp]
theorem Std.HashSet.Raw.toList_iter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.iter.toList = m.toList
source
@[simp]
theorem Std.HashSet.Raw.toListRev_iter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.iter.toListRev = m.toList.reverse
source
@[simp]
theorem Std.HashSet.Raw.toArray_iter {α : Type u} {m : Raw α} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.iter.toArray = m.toArray
source
@[simp]
theorem Std.HashSet.toList_iter {α : Type u} [BEq α] [Hashable α] {m : HashSet α} [EquivBEq α] [LawfulHashable α] :
m.iter.toList = m.toList
source
@[simp]
theorem Std.HashSet.toListRev_iter {α : Type u} [BEq α] [Hashable α] {m : HashSet α} [EquivBEq α] [LawfulHashable α] :
m.iter.toListRev = m.toList.reverse
source
@[simp]
theorem Std.HashSet.toArray_iter {α : Type u} [BEq α] [Hashable α] {m : HashSet α} [EquivBEq α] [LawfulHashable α] :
m.iter.toArray = m.toArray