PersistentHashMap iterator

This module provides an iterator for Lean.PersistentHashMap that is accessible via Lean.PersistentHashMap.iter.

inductive Lean.PersistentHashMap.Zipper (α : Type u) (β : Type v) : Type (max u v)

A zipper for traversing a PersistentHashMap. This is an inductive structure representing the remaining key-value pairs to yield.

• done {α : Type u} {β : Type v} : Zipper α β

  No more elements to yield.

• consEntries {α : Type u} {β : Type v} : Subarray (Entry α β (Node α β)) → Zipper α β → Zipper α β

  A frame of entries from a trie node.

• consCollision {α : Type u} {β : Type v} (keys : Subarray α) (vals : Subarray β) : Std.Slice.size keys = Std.Slice.size vals → Zipper α β → Zipper α β

  A frame of key-value pairs from a collision node.

def Lean.PersistentHashMap.Zipper.prependNode {α : Type u_1} {β : Type u_2} (node : Node α β) (z : Zipper α β) : Zipper α β

@[inline]

def Lean.PersistentHashMap.Zipper.step {α : Type u_1} {β : Type u_2} (it : Std.IterM Id (α × β)) : Std.IterStep (Std.IterM Id (α × β)) (α × β)

@[instance_reducible]

instance Lean.PersistentHashMap.instIterator {α : Type u_1} {β : Type u_2} : Std.Iterator (Zipper α β) Id (α × β)

@[irreducible]

def Lean.PersistentHashMap.Node.measure {α : Type u_1} {β : Type u_2} (node : Node α β) : Nat

Counts the total number of entries reachable from a node, including nested children.

def Lean.PersistentHashMap.Entry.measure {α : Type u_1} {β : Type u_2} (entry : Entry α β (Node α β)) : Nat

def Lean.PersistentHashMap.subarrayMeasure {α : Type u_1} {β : Type u_2} (es : Subarray (Entry α β (Node α β))) : Nat

Counts entries remaining in a subarray, including nested children.

def Lean.PersistentHashMap.Zipper.measure {α : Type u_1} {β : Type u_2} : Zipper α β → Nat

Counts the total remaining work in a zipper, including entries nested in child nodes.

instance Lean.PersistentHashMap.instFinite {α : Type u_1} {β : Type u_2} : Std.Iterators.Finite (Zipper α β) Id

@[instance_reducible, inline]

instance Lean.PersistentHashMap.instIteratorLoop {α : Type u_1} {β : Type u_2} {n : Type u_3 → Type u_4} [Monad n] : Std.IteratorLoop (Zipper α β) Id n

@[inline]

def Lean.PersistentHashMap.iter {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] (map : PersistentHashMap α β) : Std.Iter (α × β)

Returns a finite iterator over the key-value pairs of the given PersistentHashMap. The iteration order is unspecified.

Termination properties:

• Finite instance: always
• Productive instance: always