Iterators on HashMap and HashMap.Raw

@[inline]

def Std.HashMap.Raw.iter {α : Type u} {β : Type v} (m : Raw α β) : Iter (α × β)

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

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

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

@[inline]

def Std.HashMap.Raw.keysIter {α β : Type u} (m : Raw α β) : Iter α

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

The key and value types must live in the same universe.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• m.keysIter = m.inner.keysIter

@[inline]

def Std.HashMap.Raw.valuesIter {α β : Type u} (m : Raw α β) : Iter β

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

The key and value types must live in the same universe.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• m.valuesIter = m.inner.valuesIter

@[inline]

def Std.HashMap.iter {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : HashMap α β) : Iter (α × β)

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

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

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

@[inline]

def Std.HashMap.keysIter {α β : Type u} [BEq α] [Hashable α] (m : HashMap α β) : Iter α

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

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• m.keysIter = m.inner.keysIter

@[inline]

def Std.HashMap.valuesIter {α β : Type u} [BEq α] [Hashable α] (m : HashMap α β) : Iter β

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

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• m.valuesIter = m.inner.valuesIter