feat(cmd/simp): let `#simp` use declared `variables` (#2478)
Let `#simp` see declared `variables`.
~~Sits atop the minor `tactic.core` rearrangement in #2465.~~
@semorrison It turns out that `push_local_scope` and `pop_local_scope` weren't required; the parser is smarter than we thought, and if you declared some `variables` and then tried to `#simp` them, lean would half-know what you are talking about.
Indeed, the parsed `pexpr` from the command would include this information, but `to_expr` would report `no such 'blah'` when called afterward. To fix this you have to add the local variables you want `simp` to be able to see as local hypotheses in the same `tactic_state` in which you invoke `expr.simp`---so no wrapping your call to `expr.simp` directly in `lean.parser.of_tactic` (since this cooks up a fresh `tactic_state` for you).
Closes #2475.
<br>
<br>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
