Add function for retrieving current namespace

This is very easy. There are two options, since if we are currently in a namespace the builtin tactic.open_namespaces returns the current namespace as the first entry:

1. Modify the code so that open_namespaces prepends name.anonymous to the list it currently returns when open_namespaces is called outside any namespace, or

2. Just add a new library function to do this.

In keeping with the namespace/monad for tactic.open_namespaces, this function should have type tactic name. Note that tactic (option name) or anything of the link is unnecessary because the semantically correct value when no namespace is open is just name.anonymous.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

Start by inspecting the implementation and callers of the builtin tactic.open_namespaces, then check how namespace names and name.anonymous are represented. Add a library function with type tactic name that returns the current namespace, including name.anonymous outside a namespace, and verify it with a focused tactic test.