Commit 2023-10-20 18:15 1020213c

View on Github →

chore: refactor de-duplication in rw? (#7799) Slight refactor of how de-duplication works in rw?.

Estimated changes

Modified Mathlib/Tactic/Rewrites.lean

added def Mathlib.Tactic.Rewrites.RewriteResult.ppResult

added def Mathlib.Tactic.Rewrites.RewriteResult.prepare_ppResult

added def Mathlib.Tactic.Rewrites.rewritesDedup