Def MLList.dedup

Modification history

2025-03-04 03:24

Mathlib/Data/MLList/Dedup.lean

chore: remove >6 month old deprecations (#22473)

Deleted MLList.dedup View on Github →

2024-10-09 21:35

Mathlib/Data/MLList/Dedup.lean

chore: simplify some lambdas (#17206) …

Modified MLList.dedup View on Github →

2023-08-23 12:46

Mathlib/Data/MLList/Dedup.lean

feat: deduplicate results from rw? (#6749)

Added MLList.dedup View on Github →