Lemmas
📁 Source: Batteries/Data/Vector/Lemmas.lean
Statistics
| Metric | Count |
|---|---|
| Definitions | 0 |
TheoremsfinIdxOf?_empty, finIdxOf?_eq_none_iff, finIdxOf?_eq_some_iff, getD_mk, getElem_tail, get_cast, get_eq_getElem, get_map, get_mk, get_ofFn, get_push_castSucc, get_push_last, get_range, get_replicate, get_reverse, get_tail, isNone_finIdxOf?, isSome_finIdxOf?, tail_eq_of_ne_zero, tail_eq_of_zero, toArray_injective, toList_tail, uget_mk | 23 |
| Total | 23 |
Vector
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
finIdxOf?_empty 📖 | — | — | — | — | — |
finIdxOf?_eq_none_iff 📖 | — | — | — | — | — |
finIdxOf?_eq_some_iff 📖 | — | — | — | — | — |
getD_mk 📖 | — | — | — | — | — |
getElem_tail 📖 | — | — | — | — | tail_eq_of_ne_zero |
get_cast 📖 | — | — | — | — | — |
get_eq_getElem 📖 | — | — | — | — | — |
get_map 📖 | — | — | — | — | — |
get_mk 📖 | — | — | — | — | — |
get_ofFn 📖 | — | — | — | — | — |
get_push_castSucc 📖 | — | — | — | — | — |
get_push_last 📖 | — | — | — | — | — |
get_range 📖 | — | — | — | — | — |
get_replicate 📖 | — | — | — | — | — |
get_reverse 📖 | — | — | — | — | — |
get_tail 📖 | — | — | — | — | getElem_tail |
isNone_finIdxOf? 📖 | — | — | — | — | — |
isSome_finIdxOf? 📖 | — | — | — | — | — |
tail_eq_of_ne_zero 📖 | — | — | — | — | — |
tail_eq_of_zero 📖 | — | — | — | — | — |
toArray_injective 📖 | — | — | — | — | — |
toList_tail 📖 | — | — | — | — | — |
uget_mk 📖 | — | — | — | — | — |
---