Is `namespace` well documented somewhere?

Stream: lean4

[Valentin Robert]

I'm trying to understand why the following code works:

namespace Lean.Meta
open Elab Tactic

I'm not sure what this feature is called, where that would be documented. Definitely not in the "Functions and namespaces" page of the documentation I found.

There seems to be something happening where, when you mention the Lean.Meta namespace, it might do some amount of importing or something that makes it so that Elab and Tactic are in scope on the next line?

Does it only bring other namespaces into scope, but I still need to import modules to get their definitions in scope?

[Aaron Liu]

Does the namespace command have a docstring?

[Aaron Liu]

Valentin Robert said:

There seems to be something happening where, when you mention the Lean.Meta namespace, it might do some amount of importing or something that makes it so that Elab and Tactic are in scope on the next line?

Since Lean and Lean.Meta are open, you get to have Lean.Elab, Lean.Meta.Tactic, and Lean.Elab.Tactic.

[Valentin Robert]

Ah, part of what I was missing was that it was opening both Lean and Lean.Meta!

I was wondering why open Lean.Meta.Elab failed, but that's because in the above Elab comes out of just Lean, while Tactic comes out of Lean.Meta.

Alright, things are starting to make much more sense, and namespace does have a docstring that is pretty detailed, thanks!