Skip to content

use Lean modules in more files#912

Merged
cdisselkoen merged 1 commit intomainfrom
cdisselkoen/more-modules
Mar 18, 2026
Merged

use Lean modules in more files#912
cdisselkoen merged 1 commit intomainfrom
cdisselkoen/more-modules

Conversation

@cdisselkoen
Copy link
Contributor

Use module system in a bunch more files under Thm/SymCC (but not yet all files in that directory).

No significant refactors other than visibility tweaks and some workarounds for certain internal definitions not being exposed even with import all.

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
@cdisselkoen cdisselkoen merged commit ddcec57 into main Mar 18, 2026
13 checks passed
@cdisselkoen cdisselkoen deleted the cdisselkoen/more-modules branch March 18, 2026 18:51
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.

3 participants