Iterators on HashSet and HashSet.Raw

@[inline]

def Std.HashSet.Raw.iter {α : Type u} (m : Raw α) : Iter α

Returns a finite iterator over the elements of a hash set. The iterator yields the elements of the set in order and then terminates.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• m.iter = Std.Iterators.Iter.map (fun (e : (_ : α) × Unit) => e.fst) m.inner.inner.iter

@[inline]

def Std.HashSet.iter {α : Type u} [BEq α] [Hashable α] (m : HashSet α) : Iter α

Returns a finite iterator over the elements of a hash set. The iterator yields the elements of the set in order and then terminates.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• m.iter = Std.Iterators.Iter.map (fun (e : (_ : α) × Unit) => e.fst) m.inner.inner.iter