Merged
Conversation
…_gen (#136) Add checkCategoryNamesAvailable that verifies none of the category names about to be introduced by #strata_gen already exist in the Lean environment. Reports a clear error message for each collision and aborts generation.
MikaelMayer
commented
Apr 1, 2026
Contributor
Author
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Clean, well-scoped change. The pre-check mirrors the name resolution logic used during generation, the error message is actionable, and the test covers the private-name scenario. One minor duplication note inline.
tautschnig
approved these changes
Apr 3, 2026
joehendrix
approved these changes
Apr 3, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
#strata_gendid not check whether the datatype names it was about to introduce already existed in the Lean environment, leading to confusing errors from the elaborator.This adds a pre-generation check that resolves each category name (respecting the current namespace and private name mangling) and verifies it is not already defined. When a conflict is found, a clear error message is reported and code generation is aborted.
The name-resolution logic is factored into a shared
resolveScopedNamehelper used by bothmkScopedIdentand the new availability check.Tested: existing tests pass, new test added for the duplicate name scenario.
Fixes #136