Commit 2023-08-29 00:54 0a43d126

View on Github →

chore: fix bug in rw? (#6088) This fixes a problem I encountered in another tactic, where the rewrites are not being tried with the original MetavarContext.

Estimated changes

Modified Mathlib/Tactic/Rewrites.lean

Modified test/rewrites.lean

added def zero