From d8bcd6a32ee3b7a37dc2e823840232052aefae8d Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 23 Jan 2025 07:47:38 +0000 Subject: [PATCH] doc: correspondence `ModuleIdx` <--> `Environment.moduleNames` (#6749) 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! --- src/Lean/Environment.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 5a9488ed65..b4c5662fd7 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -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 := #[]