max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: correspondence ModuleIdx <--> Environment.moduleNames (#6749)

Browse source 
This PR documents the equality between the `ModuleIdx` of an module and
the index in the array of `moduleNames` of the same module.

I asked about this in the Office hours and it was confirmed that this is
a current feature and one that is likely not to change!
This commit is contained in:
damiano 2025-01-23 07:47:38 +00:00 • committed by GitHub
parent f35a602070
commit d8bcd6a32e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Environment.lean
View file

@ -141,7 +141,10 @@ structure EnvironmentHeader where
imports : Array Import := #[]
/-- Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management. -/
regions : Array CompactedRegion := #[]
/-- Name of all imported modules (directly and indirectly). -/
/--
Name of all imported modules (directly and indirectly).
The index of a module name in the array equals the `ModuleIdx` for the same module.
-/
moduleNames : Array Name := #[]
/-- Module data for all imported modules. -/
moduleData : Array ModuleData := #[]