Commit 2023-06-21 01:19 cef370e3

View on Github →

feat: rewrites at location (#4157)

Estimated changes

Modified Mathlib/Tactic/Rewrites.lean

Modified Mathlib/Tactic/TryThis.lean

modified def addRewriteSuggestion

Modified test/rewrites.lean