Skip to content

Commit ac1e606

Browse files
authored
chore: document ir.sig, update module system reference (#872)
1 parent 116c7fb commit ac1e606

2 files changed

Lines changed: 8 additions & 2 deletions

File tree

Manual/BuildTools/Lake.lean

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -485,6 +485,7 @@ module.importInfo
485485
module.imports
486486
module.input
487487
module.ir
488+
module.ir.sig
488489
module.lean
489490
module.leanArts
490491
module.ltar
@@ -556,7 +557,12 @@ The facets available for modules are:
556557

557558
: `ir`
558559

559-
The `.ir` file produced by `lean` (with the {ref "module-structure"}[experimental module system] enabled).
560+
The `.ir` file produced for modules that use the {ref "module-structure"}[module system].
561+
562+
563+
: `ir.sig`
564+
565+
The `.ir.sig` file produced for modules that use the {ref "module-structure"}[module system].
560566

561567
: `c`
562568

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:nightly-2026-06-22
1+
leanprover/lean4:nightly-2026-06-25

0 commit comments

Comments
 (0)