Commit 2020-04-24 01:03 02d73084

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>