Ordering of modules: `moduleNames` vs `ModuleIdx`

Stream: lean4

[Damiano Testa]

The docs#Lean.EnvironmentHeader contains a moduleNames field that is an Array of Names containing all (transitively) imported module names of the current file.

[Damiano Testa]

For most functions, though, Lean refers to imported modules not by Name, but by docs#Lean.ModuleIdx, a type alias of Nat.

[Damiano Testa]

This means that it is easy to find the index of a module, but you then have to convert this index to a Name in some way.

[Damiano Testa]

Empirically, the order of the module names in moduleNames is exactly the ModuleIdx of the module.

[Damiano Testa]

Was I lucky? :smile:

[Damiano Testa]

Can I count on this?

[Damiano Testa]

Should this be documented?

[Damiano Testa]

(This question came from the comments to #20908 that exploits this "feature".)

[Damiano Testa]

Answered during office hours: the correspondence of ModuleIdx and "index in the array of module names" has been around for a long time and is also used by doc-gen.

[Damiano Testa]

lean4#6749

[Damiano Testa]

Kyle mentioned also docs#Lean.findModuleOf?, which was a perfect fit for my application.