Documentation
Mathlib
.
Data
.
MLList
.
Dedup
Search
Google site search
return to top
source
Imports
Init
Batteries.Data.HashMap.Basic
Batteries.Data.MLList.Basic
Imported by
MLList
.
dedupBy
MLList
.
dedup
Lazy deduplication of lazy lists
#
source
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.
Instances For
source
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
fun (
b
:
β
) =>
pure
b
Instances For