f85c66789d
This PR replaces `Array.feraseIdx` and `Array.insertAt` with `Array.eraseIdx` and `Array.insertIdx`, both of which take a `Nat` argument and a tactic-provided proof that it is in bounds. We also have `eraseIdxIfInBounds` and `insertIdxIfInBounds` which are noops if the index is out of bounds. We also provide a `Fin` valued version of `Array.findIdx?`. Together, these quite ergonomically improve the array indexing safety at a number of places in the compiler/elaborator. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||