Commit 2023-08-23 12:46 c35ba473

View on Github →

feat: deduplicate results from rw? (#6749)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/MLList/Dedup.lean

added def MLList.dedup

added def MLList.dedupBy

Modified Mathlib/Tactic/Rewrites.lean

Modified test/rewrites.lean