# Iterators on `DHashMap` and `DHashMap.Raw` #

source
@[inline]
def Std.DHashMap.Raw.iter {α : Type u} {β : α → Type v} (m : Raw α β) :
Iter ((a : α) × β a)

Returns a finite iterator over the entries of a dependent 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.flatMap (fun (b : Std.DHashMap.Internal.AssocList α β) => b.iter) m.buckets.iter

Instances For

source
@[inline]
def Std.DHashMap.Raw.keysIter {α : Type u} {β : α → Type u} (m : Raw α β) :
Iter α

Returns a finite iterator over the keys of a dependent 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 = Std.Iterators.Iter.map (fun (e : (a : α) × β a) => e.fst) m.iter

Instances For

source
@[inline]
def Std.DHashMap.Raw.valuesIter {α β : Type u} (m : Raw α fun (x : α) => β) :
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 = Std.Iterators.Iter.map (fun (e : (_ : α) × β) => e.snd) m.iter

Instances For

source
@[inline]
def Std.DHashMap.iter {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : DHashMap α β) :
Iter ((a : α) × β a)

Returns a finite iterator over the entries of a dependent 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 = m.inner.iter

Instances For

source
@[inline]
def Std.DHashMap.keysIter {α : Type u} {β : α → Type u} [BEq α] [Hashable α] (m : DHashMap α β) :
Iter α

Returns a finite iterator over the keys of a dependent 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

Instances For

source
@[inline]
def Std.DHashMap.valuesIter {α β : Type u} [BEq α] [Hashable α] (m : DHashMap α fun (x : α) => β) :
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 = Std.Iterators.Iter.map (fun (e : (_ : α) × β) => e.snd) m.iter

Instances For