Skip to content

Guard gen_degree emit behind __main__ - #2

Open
Chessing234 wants to merge 1 commit into
teorth:masterfrom
Chessing234:fix/gen-degree-main-guard
Open

Chessing234 wants to merge 1 commit into
teorth:masterfrom
Chessing234:fix/gen-degree-main-guard

Conversation

@Chessing234

Copy link
Copy Markdown

Summary

  • scripts/gen_degree.py had its Lean-emit block at module scope after if __name__ == "__main__":, so import gen_degree immediately raised NameError: name 'n' is not defined.
  • Indent the emit block under __main__ so the module is importable; script behavior unchanged when run as python scripts/gen_degree.py N.

Test plan

  • Before: importlib load of gen_degree.py → NameError: n
  • After: import succeeds and exposes Ppoly; ast.parse clean

Made with Cursor

Code after the main guard still ran at import time and required n, so
importing gen_degree raised NameError. Indent the emit block under
__main__ so the module loads cleanly.
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