Lazy deduplication of lazy lists

Deprecation

This material has been moved out of Mathlib to https://github.com/semorrison/lean-monadic-list.

@[deprecated]

def MLList.dedupBy {α : Type} {β : Type} {m : Type → Type} [Monad m] [BEq β] [Hashable β] (L : MLList m α) (f : α → m β) : MLList m α

Lazily deduplicate a lazy list, using a stored HashMap.

Equations

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

@[deprecated]

def MLList.dedup {β : Type} {m : Type → Type} [Monad m] [BEq β] [Hashable β] (L : MLList m β) : MLList m β

Lazily deduplicate a lazy list, using a stored HashMap.

Equations

• L.dedup = L.dedupBy pure