RFC: let `export` create namespace aliases

Stream: lean4

[Kyle Miller]

lean4#6394 has an RFC to make it possible to export entire namespaces, and to give export some open-like variations (being able to name the aliases and being able to hide certain aliases).

Something this fixes is the following issue. Currently, the last line here gives an "unknown constant" error.

namespace NS
inductive T
  | mk
end NS

export NS (T)

#check T -- NS.T
#check T.mk -- error: unknown constant

However, with the RFC the name T.mk would resolve to NS.T.mk.

[Kyle Miller]

Another motivation for this is that at some point we will be able to configure dot notation (perhaps with lean4#6267), which will let us create libraries of generic functions meant to be used with dot notation. With a namespace export, one can simply write export FnsForDotNotation from within a given concrete type's namespace, and this will make all names in FnsForDotNotation immediately and permanently available, without needing to give the names of the individual functions, and also any future additions to FnsForDotNotation would be available as well.

[Kyle Miller]

Comments or questions welcome!

[Edward van de Meent]

i think this is a great idea! i was surprised this didn't already work.

[Edward van de Meent]

(be sure to :+1: the issue if you think this is important)

[Jireh Loreaux]

Kyle, does the export NS (T) above export that namespace for all eternity? What I mean is: if later I write:

namespace NS
lemma T.foo : True := True.intro
end NS

#check T.foo -- this works? or not?

[Kyle Miller]

Yes, that works.