Iterators on DTreeMap

@[inline]

def Std.TreeSet.iter {α : Type u} {cmp : α → α → Ordering} (m : TreeSet α cmp) : Iter α

Returns a finite iterator over the entries of a tree 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.iter

@[simp]

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