Commit 2019-06-08 23:11 3f9916e1
View on Github →feat(tactic/rewrite_all): tactic to perform the nth occurrence of a rewrite (#999)
- feat(tactic/rewrite_all): tactic to perform the nth occurrence of a rewrite
- formatting
- formatting
- perhaps a little bit easier to read?
- try renaming
- there was a duplicate definition, just not the one lean complained about
- Namespaces
- I think kabstract works now
- Fix
- Test
- Fix guard
- updating test to reflect difference between congr and kabstract
- oops
- adding Keeley's example
- remove kabstract implementation for now
- cleanup test file
- rename common to basic
- Update src/tactic/rewrite_all/default.lean