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

doc: update const2ModIdx docstring

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-25 14:06:07 -07:00
parent 236885e72e
commit dadfe84c15
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Environment.lean
View file

@ -113,6 +113,10 @@ structure Environment where
Recall that a Leah file has a header where previously compiled modules can be imported.
Each imported module has a unique `ModuleIdx`.
Many extensions use the `ModuleIdx` to efficiently retrieve information stored in imported modules.
Remark: this mapping also contains auxiliary constants, created by the code generator, that are **not** in
the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator.
Only the code generator uses them.
-/
const2ModIdx : HashMap Name ModuleIdx
/--