Namespace Questions: re-exporting, attrubutes, etc.

Stream: lean4

[Joey Eremondi]

I'm trying to better understand scopes and namespaces, and I've got a bunch of questions about them:

1. Is there a way to re-export names from a structure into a namespace? For example, if I've got

namespace Foo
structure Bar : Type where
  baz : Nat
open Bar

I want baz to be in the namespace Foo, so whenever someone does open Foo they can write baz instead of Bar.baz.

2. More generally, is there a way to import one module and re-export its values? I.e. can I define a module that just imports a bunch of other modules and re-exports them into a single module, so they can all be imported at once?

3. How do attributes interact with namespaces, specifically simp and aesop? If I've declared a rule as having the simp attribute, and that definition was in namespace Foo and module M, do you have to have both import M and open Foo for the simp rule to be used?

[Jon Eugster]

1) I've seen the pattern

namespace Foo
structure Bar : Type where
  baz : Nat

abbrev baz := Bar.baz

before. Not sure if there's a better method.

2) would that not just be a lean file with only imports, like for example Mathlib.Tactics.Common?

3) no, you don't need to open a namespace for a simp-lemma to be found.

[Eric Wieser]

I think you can use export Bar (baz) which avoids having a second declaration

[Joey Eremondi]

Ooh, did not know there was an export keyword, will have to look at the docs for this

[James Gallicchio]

also, lean files are called modules by lake, but have very little to do with modules from ML. namespaces are global and are not first-class (in the sense that you cannot operate on them like ML modules).

I think the FRO has long-term thoughts about adding modules akin to those in ML and Roq, but last I heard it is a ways off!

[Kyle Miller]

Joey Eremondi said:

3. How do attributes interact with namespaces

Each attribute is free to have its own implementation for how it works, but I believe this is the expectation:

• If a global attribute is added in module A, then when you import module A you import that global attribute.
• If a scoped attribute is added in namespace NS in module A, then when you import module A you have to do open scoped NS (or the full open NS) to activate the scoped attribute.

For importing, only scoped attributes have any interaction with namespaces.

[Kyle Miller]

There's risk of confusion here between the attribute itself and an attribute applied to a declaration. I'm not sure if we have terminology to distinguish them... In any case, some attributes support scoping, others don't, and when I say "scoped attribute" I mean specifically that an attribute-supporting-scoping was applied to a declaration by using the scoped modifier. (And if you don't use scoped or local, the attribute applied as global.)