Lazy deduplication of lazy lists

Deprecation

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

@[deprecated "See deprecation note in module documentation." (since := "2024-08-22")]

def MLList.dedupBy {α β : 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 "See deprecation note in module documentation." (since := "2024-08-22")]

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