Mathlib v3 is deprecated. Go to Mathlib v4

Inductive expr_lens.dir

Modification history

2020-04-26 06:46
src/meta/expr_lens.lean
refactor(tactic/nth_rewrite): enable rewriting hypotheses, add docstrings (#2471) …
Added expr_lens.dirView on Github →