Commit 2020-04-21 17:16 ffa97d0f

fix(tactic/where): remove hackery from #where, using Lean 3c APIs (#2465) We remove almost all of the hackery from #where, using the Lean 3c APIs exposed by @cipher1024. In doing so we add pair of library functions which make this a tad more convenient. The last "hack" which remains is by far the most mild; we expose lean.parser.get_current_namespace, which creates a dummy definition in the environment in order to obtain the current namespace. Of course this should be replaced with an exposed C++ function when the time comes (crossref with the leanprover-community/lean issue here: https://github.com/leanprover-community/lean/issues/196).