Iterators on associative lists

@[unbox]

structure Std.DHashMap.Internal.AssocList.AssocListIterator (α : Type u) (β : α → Type v) : Type (max u v)

Internal implementation detail of the hash map

• l : AssocList α β

theorem Std.DHashMap.Internal.AssocList.AssocListIterator.ext_iff {α : Type u} {β : α → Type v} {x y : AssocListIterator α β} : x = y ↔ x.l = y.l

theorem Std.DHashMap.Internal.AssocList.AssocListIterator.ext {α : Type u} {β : α → Type v} {x y : AssocListIterator α β} (l : x.l = y.l) : x = y

@[instance_reducible]

instance Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma {α : Type u_1} {β : α → Type u_2} : Iterator (AssocListIterator α β) Id ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.

instance Std.DHashMap.Internal.AssocList.instFiniteAssocListIteratorIdSigma {α : Type u_1} {β : α → Type u_2} : Iterators.Finite (AssocListIterator α β) Id

@[instance_reducible]

instance Std.DHashMap.Internal.AssocList.instIteratorLoopAssocListIteratorIdSigmaOfMonad {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] : IteratorLoop (AssocListIterator α β) Id m

Equations

• Std.DHashMap.Internal.AssocList.instIteratorLoopAssocListIteratorIdSigmaOfMonad = Std.IteratorLoop.defaultImplementation

def Std.DHashMap.Internal.AssocList.iter {α : Type u} {β : α → Type v} (l : AssocList α β) : Iter ((a : α) × β a)

Internal implementation detail of the hash map. Returns a finite iterator on an associative list.

Equations

• l.iter = { internalState := { l := l } }