lean4
lean4 copied to clipboard
Published
20 hours ago •
leanprover
leanprover
feat: add `inductive.autoPromoteIndices` option
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
Mathlib CI status (docs):
- ✅ Mathlib branch lean-pr-testing-3590 has successfully built against this PR. (2024-03-04 12:37:16) View Log
- 🟡 Mathlib branch lean-pr-testing-3590 build against this PR was cancelled. (2024-03-04 13:13:02) View Log
- ✅ Mathlib branch lean-pr-testing-3590 has successfully built against this PR. (2024-03-04 14:23:09) View Log
- 🟡 Mathlib branch lean-pr-testing-3590 build against this PR was cancelled. (2024-03-04 18:59:36) View Log
- ✅ Mathlib branch lean-pr-testing-3590 has successfully built against this PR. (2024-03-04 20:10:21) View Log
