Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes