6ad28ca446
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` |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||