mathlib3

ffa97d0f - fix(tactic/where): remove hackery from `#where`, using Lean 3c APIs (#2465)

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). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>