Lemmas
📁 Source: Batteries/Data/Array/Lemmas.lean
Statistics
Array
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
eraseP_toArray 📖 | — | — | — | — | — |
erase_toArray 📖 | — | — | — | — | — |
extract_append_of_size_left_le_start 📖 | — | — | — | — | — |
extract_append_of_stop_le_size_left 📖 | — | — | — | — | — |
extract_empty_of_start_eq_stop 📖 | — | — | — | — | — |
extract_eq_of_size_le_stop 📖 | — | — | — | — | — |
forIn_eq_forIn_toList 📖 | — | — | — | — | — |
getElem_insertIdx_eq 📖 | — | — | — | — | — |
getElem_insertIdx_gt 📖 | — | — | — | — | — |
getElem_insertIdx_lt 📖 | — | — | — | — | — |
idxOf?_toList 📖 | — | — | — | — | — |
size_eraseIdxIfInBounds 📖 | — | — | — | — | — |
size_set! 📖 | — | — | — | — | — |
toList_drop 📖 | — | — | — | — | — |
toList_erase 📖 | — | — | — | — | — |
---