Documentation

Mathlib.Data.MLList.Dedup

Lazy deduplication of lazy lists #

def MLList.dedupBy {m : TypeType} {β : Type} [Monad m] [BEq β] [Hashable β] {α : Type} (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.
Instances For
    def MLList.dedup {m : TypeType} {β : Type} [Monad m] [BEq β] [Hashable β] (L : MLList m β) :
    MLList m β

    Lazily deduplicate a lazy list, using a stored HashMap.

    Equations
    • L.dedup = L.dedupBy fun (b : β) => pure b
    Instances For