-
Notifications
You must be signed in to change notification settings - Fork 388
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
fix: Incorrect promotion from index to paramater #3591
Conversation
Mathlib CI status (docs):
|
src/Lean/Elab/Inductive.lean
Outdated
@@ -25,6 +25,11 @@ open Meta | |||
builtin_initialize | |||
registerTraceClass `Elab.inductive | |||
|
|||
register_builtin_option autoPromoteIndices : Bool := { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
register_builtin_option autoPromoteIndices : Bool := { | |
register_builtin_option inductive.autoPromoteIndices : Bool := { |
seems like it should be scoped in some way, although I'm really missing that option naming style guide 😭
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree. Fixed in the relevant PR #3590.
06193e6
to
fea6fef
Compare
@arthur-adjedj, I've sent #3590 to the merge queue now. Please ping me when this one is ready to go. |
This PR partly addresses #3458, by adding an option `autoPromoteIndices` to turn off the promotion of fixed indices to parameters. The actual fix for the issue is in a separate PR #3591. Because nested inductive datatypes parameters cannot contain local variables, it is often desirable for a fixed index to not be promoted, as to allow free variables in that place. See example in `3458_1.lean`
@semorrison This PR is in a ready state. My only worry is that the added condition to |
!bench |
Here are the benchmark results for commit 19a9de4. |
Sorry it took a while to get back to this. |
Depends on #3590
Closes #3458