[ elab ] Let elab scripts access visibility modifiers

[jacobjwalters]

Description

This is a small extension to the elaborator that allows an elab script to query the visibility of a declaration.

As a quick example, given the following file:

private foo : Bar
export baz : Quux
namespace A
  public export foo : Bar

We can get do the following in the REPL:

> :let %language ElabReflection
> %runElab getVis `{foo}
[(NS (MkNS ["A", "Main"]) (UN (Basic "foo")), Public),
 (NS (MkNS ["Main"]) (UN (Basic "foo")), Private)]
> %runElab getVis `{baz}
[(NS (MkNS ["Main"]) (UN (Basic "baz")), Export)]

The visibilities of all declarations matching the given Name are returned.

Should this change go in the CHANGELOG?

• [x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[andrevidela]

I don't know if I can do this for you, but if you rebase from main you should be able to get all the tests pass

[andrevidela]

LGTM