Iterators on DTreeMap

@[inline]

def Std.DTreeMap.iter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (m : DTreeMap α β cmp) : Iter ((a : α) × β a)

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

@[inline]

def Std.DTreeMap.keysIter {α : Type u} {β : α → Type u} {cmp : α → α → Ordering} (m : DTreeMap α β cmp) : Iter α

Returns a finite iterator over the keys of a dependent tree 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 = { inner := m.inner }.keysIter

@[inline]

def Std.DTreeMap.valuesIter {α β : Type u} {cmp : α → α → Ordering} (m : DTreeMap α (fun (x : α) => β) cmp) : Iter β

Returns a finite iterator over the values of a tree 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 = { inner := m.inner }.valuesIter

@[simp]

theorem Std.DTreeMap.toList_iter {α : Type u_1} {β : α → Type u_2} {cmp : α → α → Ordering} (m : DTreeMap α β cmp) : m.iter.toList = m.toList

@[simp]

theorem Std.DTreeMap.keysIter_toList {α : Type u_1} {β : α → Type u_1} {cmp : α → α → Ordering} (m : DTreeMap α β cmp) : m.keysIter.toList = m.keys

@[simp]

theorem Std.DTreeMap.valuesIter_toList {α β : Type u_1} {cmp : α → α → Ordering} (m : DTreeMap α (fun (x : α) => β) cmp) : m.valuesIter.toList = m.values