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 Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma {α : Type u_1} {β : α → Type u_2} : Iterators.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 Std.DHashMap.Internal.AssocList.instIteratorCollectAssocListIteratorIdSigmaOfMonad {α : Type u} {β : α → Type v} {m : Type (max u v) → Type w''} [Monad m] : Iterators.IteratorCollect (AssocListIterator α β) Id m

Equations

• Std.DHashMap.Internal.AssocList.instIteratorCollectAssocListIteratorIdSigmaOfMonad = Std.Iterators.IteratorCollect.defaultImplementation

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

Equations

• Std.DHashMap.Internal.AssocList.instIteratorCollectPartialAssocListIteratorIdSigmaOfMonad = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

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

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

Equations

• Std.DHashMap.Internal.AssocList.instIteratorLoopPartialAssocListIteratorIdSigmaOfMonad = Std.Iterators.IteratorLoopPartial.defaultImplementation

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

Equations

• Std.DHashMap.Internal.AssocList.instIteratorSizeAssocListIteratorIdSigma = Std.Iterators.IteratorSize.defaultImplementation

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

Equations

• Std.DHashMap.Internal.AssocList.instIteratorSizePartialAssocListIteratorIdSigma = Std.Iterators.IteratorSizePartial.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 } }