Commit 2020-03-31 14:30 b508d0e0
View on Github →feat(tactic/equiv_rw): rewriting along equivalences (#2246)
- feat(tactic): rewriting along equivalences
- header
- minor
- type
- actually, rewriting the goal under functors is easy
- rewriting inside function types
- more
- way better
- improving comments
- fun
- feat(data/equiv): pi_congr
- various
- feat(data/equiv): sigma_congr
- docstrings
- change case for consistency
- tidying up
- minor
- minor
- switching names
- fixes
- add some tracing routines for convenience
- feat(tactic/core): trace_for
- typo
- oops
- oops
- various
- chore(tactic/solve_by_elim): cleanup
- cleanup
- what happened to my commit?
- fix
- fix
- rename to trace_if_enabled
- fixed?
- Tweak comments
- feat(tactic/solve_by_elim): add accept parameter to prune tree search
- when called with empty lemmas, use the same default set as the interactive tactic
- trace_state_if_enabled
- Update src/data/equiv/basic.lean
- implicit arguments
- stop cheating with [] ~ none
- indenting
- yay, working via solve_by_elim
- pretty good
- various
- various
- docstring
- fix docstrings
- more docs
- docs
- feat(data/equiv/functor): bifunctor.map_equiv
- bifunctors
- test rewriting under unique
- rewriting in subtypes
- add documentation, and make the function an explicit argument
- documentation
- fix doc-strings
- typos
- minor
- adding demonstration of transporting semigroup
- Update .vscode/settings.json
- err
- trying to transport through monoid
- err?
- much better
- improve documentation of accept, and add doc-string
- fix duplicated namespace
- improve docs
- try again with documentation
- update
- oops
- rename adapt_equiv
- simplify the equivalence produced, and provide a tactic to access the equivalence
- add max_steps option
- add decl_name to add_tactic_doc
- fix add_tactic_doc
- satisfying linter
- add defaults for cfg arguments
- remove simplify_term, which already existed as expr.simp
- remove duplicate functions that have been PRd separately
- no need for accept
- Update src/tactic/equiv_rw.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
- Update src/tactic/equiv_rw.lean Co-Authored-By: Gabriel Ebner gebner@gebner.org
- replace max_steps with max_depth
- use solve_aux
- add missing simp lemmas about arrow_congr'
- fix failing test, by making sure we don't leave any ≃ goals on the table
- add comment
- comment out trace output