@[inline]

def Std.IterM.toHashSet {α β : Type w} [BEq β] [Hashable β] {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) : m (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 α m, the variant {lean}it.ensureTermination.toHashSet always terminates after finitely many steps.

Equations

• it.toHashSet = Std.IterM.fold (fun (acc : Std.HashSet β) (a : β) => acc.insert a) ∅ it

@[inline]

def Std.IterM.Total.toHashSet {α β : Type w} [BEq β] [Hashable β] {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] (it : Total m β) : m (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 IterM.toHashSet.

Equations

• it.toHashSet = it.it.toHashSet

@[inline]

def Std.IterM.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β] {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) : m (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 α m, the variant {lean}it.ensureTermination.toExtHashSet always terminates after finitely many steps.

Equations

• it.toExtHashSet = Std.IterM.fold (fun (acc : Std.ExtHashSet β) (a : β) => acc.insert a) ∅ it

@[inline]

def Std.IterM.Total.toExtHashSet {α β : Type w} [BEq β] [Hashable β] [EquivBEq β] [LawfulHashable β] {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] (it : Total m β) : m (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 IterM.toExtHashSet.

Equations

• it.toExtHashSet = it.it.toExtHashSet

@[inline]

def Std.IterM.toTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) (cmp : β → β → Ordering) : m (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 α m, the variant {lean}it.ensureTermination.toTreeSet always terminates after finitely many steps.

Equations

• it.toTreeSet cmp = Std.IterM.fold (fun (acc : Std.TreeSet β cmp) (a : β) => acc.insert a) ∅ it

@[inline]

def Std.IterM.Total.toTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] (it : Total m β) (cmp : β → β → Ordering) : m (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 IterM.toTreeSet.

Equations

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

@[inline]

def Std.IterM.toExtTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [IteratorLoop α m m] (it : IterM m β) (cmp : β → β → Ordering := by exact compare) [TransCmp cmp] : m (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 α m, the variant {lean}it.ensureTermination.toExtTreeSet cmp always terminates after finitely many steps.

Equations

• it.toExtTreeSet cmp = Std.IterM.fold (fun (acc : Std.ExtTreeSet β cmp) (a : β) => acc.insert a) ∅ it

@[inline]

def Std.IterM.Total.toExtTreeSet {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Iterators.Finite α m] [IteratorLoop α m m] (it : Total m β) (cmp : β → β → Ordering := by exact compare) [TransCmp cmp] : m (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 IterM.toExtTreeSet.

Equations

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