Skip to content

feat: #min_imports in the module system - #168

Open
thorimur wants to merge 29 commits into
leanprover-community:mainfrom
thorimur:min-imports-module
Open

thorimur wants to merge 29 commits into
leanprover-community:mainfrom
thorimur:min-imports-module

Conversation

@thorimur

@thorimur thorimur commented Oct 2, 2026 •

Copy link
Copy Markdown
Collaborator

This PR upgrades #min_imports to function in the module system.

It also includes an ergonomic upgrade: #min_imports can now be run from any point in the file, and will take into account the declarations in the entire file, including those which come after it.


@thorimur thorimur mentioned this pull request Oct 2, 2026
@thorimur
thorimur marked this pull request as ready for review October 2, 2026 23:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant