8e96d7ba1d
- Removes the public definitions `Array.eraseIdxAux` and `Array.eraseIdxSzAux` which were implementation details. - Motivation: `Array.eraseIdxAux` and `Array.eraseIdxSzAux` were clearly not intended to remain public, but simply making them private would make it inconvenient to unfold them when writing proofs in Std. - Adds documentation comments to the public `Array.eraseIdx`-related definitions which remain. - Removes `Array.eraseIdx'` which was just `Array.feraseIdx` wrapped in a subtype and adds `Array.size_feraseIdx` to prove the subtype property as a standalone theorem. Co-Authored-By: Daniel Windham <daniel@atlascomputing.org> |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| BasicAux.lean | ||
| BinSearch.lean | ||
| DecidableEq.lean | ||
| InsertionSort.lean | ||
| Lemmas.lean | ||
| Mem.lean | ||
| QSort.lean | ||
| Subarray.lean | ||