Commit 2023-08-29 13:52 cac4c90d

View on Github →

feat: rw? uses local hypotheses (#6764)

Estimated changes

Modified Mathlib/Tactic/Rewrites.lean

added def Mathlib.Tactic.Rewrites.backwardWeight

added def Mathlib.Tactic.Rewrites.forwardWeight

added def Mathlib.Tactic.Rewrites.localHypotheses

modified def Mathlib.Tactic.Rewrites.rewrites

modified def Mathlib.Tactic.Rewrites.rewritesCore

Modified test/rewrites.lean