Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-26 06:46 1182e910

View on Github →

refactor(tactic/nth_rewrite): enable rewriting hypotheses, add docstrings (#2471) This PR

  • renames the interactive tactic perform_nth_rewrite to nth_rewrite
  • enables rewriting at hypotheses, instead of only the target
  • renames the directory and namespace rewrite_all to nth_rewrite
  • adds a bunch of docstrings

Estimated changes

added inductive expr_lens.dir