Skip to content

v0.1.14

Choose a tag to compare

@github-actions github-actions released this 26 May 21:19
· 138 commits to main since this release

Module-system headers in info-tree processing

process_module_with_info_tree now handles Lean 4's module-system headers: the module keyword, public import,
ordinary private-scope imports, and import all. Files using import all now resolve the named module instead of
surfacing unknown module prefix 'all', and userImports / missingImports report the bare module names just as the
legacy header path does.