@[inline]

def Std.Iter.toHashSet {α β : Type w} [BEq β] [Hashable β] [Iterator α Id β] [IteratorLoop α Id Id] (it : Iter β) : HashSet β

Traverses the given iterator and stores the emitted values in a {name}HashSet.

If the iterator is not finite, this function might run forever. Given {givenInstance}Finite α Id, the variant {lean}it.ensureTermination.toHashSet always terminates after finitely many steps.

Equations

• it.toHashSet = it.toIterM.toHashSet.run

@[inline]

def Std.Iter.Total.toHashSet {α β : Type w} [BEq β] [Hashable β] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] (it : Total β) : HashSet β

Traverses the given iterator and stores the emitted values in a HashSet.

This variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.toHashSet.

Equations

• it.toHashSet = it.it.toHashSet

@[inline]

def Std.Iter.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β] [Iterator α Id β] [IteratorLoop α Id Id] (it : Iter β) : ExtHashSet β

Traverses the given iterator and stores the emitted values in a {name}ExtHashSet.

If the iterator is not finite, this function might run forever. Given {givenInstance}Finite α Id, the variant {lean}it.ensureTermination.toExtHashSet always terminates after finitely many steps.

Equations

• it.toExtHashSet = it.toIterM.toExtHashSet.run

@[inline]

def Std.Iter.Total.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β] [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] (it : Total β) : ExtHashSet β

Traverses the given iterator and stores the emitted values in a ExtHashSet.

This variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.toExtHashSet.

Equations

• it.toExtHashSet = it.it.toExtHashSet

@[inline]

def Std.Iter.toTreeSet {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] (it : Iter β) (cmp : β → β → Ordering := by exact compare) : TreeSet β cmp

Traverses the given iterator and stores the emitted values in a {name}TreeSet.

If the iterator is not finite, this function might run forever. Given {givenInstance}Finite α Id, the variant {lean}it.ensureTermination.toTreeSet cmp always terminates after finitely many steps.

Equations

• it.toTreeSet cmp = (it.toIterM.toTreeSet cmp).run

@[inline]

def Std.Iter.Total.toTreeSet {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] (it : Total β) (cmp : β → β → Ordering := by exact compare) : TreeSet β cmp

Traverses the given iterator and stores the emitted values in a TreeSet.

This variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.toTreeSet.

Equations

• it.toTreeSet cmp = it.it.toTreeSet cmp

@[inline]

def Std.Iter.toExtTreeSet {α β : Type w} [Iterator α Id β] [IteratorLoop α Id Id] (it : Iter β) (cmp : β → β → Ordering := by exact compare) [TransCmp cmp] : ExtTreeSet β cmp

Traverses the given iterator and stores the emitted values in a {name}ExtTreeSet.

If the iterator is not finite, this function might run forever. Given {givenInstance}Finite α Id, the variant {lean}it.ensureTermination.toExtTreeSet cmp always terminates after finitely many steps.

Equations

• it.toExtTreeSet cmp = (it.toIterM.toExtTreeSet cmp).run

@[inline]

def Std.Iter.Total.toExtTreeSet {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] [IteratorLoop α Id Id] (it : Total β) (cmp : β → β → Ordering := by exact compare) [TransCmp cmp] : ExtTreeSet β cmp

Traverses the given iterator and stores the emitted values in a ExtTreeSet.

This variant terminates after finitely many steps and requires a proof that the iterator is finite. If such a proof is not available, consider using Iter.toExtTreeSet.

Equations

• it.toExtTreeSet cmp = it.it.toExtTreeSet cmp