Documentation Verification Report

Basic

📁 Source: Batteries/Data/Array/Basic.lean

Statistics

MetricCount
DefinitionsequalSet, max?, maxD, maxI, maxWith, min?, minD, minI, minWith, scanl, scanlM, loop, scanr, scanrM, loop, setN, contains, isEmpty, popHead?, scanl, scanlM, scanr, scanrM
23
Theorems0
Total23

Array

Definitions

NameCategoryTheorems
equalSet 📖CompOp
max? 📖CompOp
maxD 📖CompOp
maxI 📖CompOp
maxWith 📖CompOp
min? 📖CompOp
minD 📖CompOp
minI 📖CompOp
minWith 📖CompOp
scanl 📖CompOp
22 mathmath: scanl_eq_singleton_iff, scanl_reverse, getElem?_scanl_zero, scanl_push, take_scanl, scanl_singleton, scanl_map, scanl_empty, scanl_eq_scanlM, Subarray.scanl_eq_scanl_extract, getElem?_scanl, back_scanl, toList_scanl, size_scanl, scanlM_pure, getElem?_succ_scanl, List.toArray_scanl, idRun_scanlM, getElem_scanl_zero, back_scanl?, scanl_eq_scanl_toList, scanl_extract
scanlM 📖CompOp
11 mathmath: scanlM_reverse, scanl_eq_scanlM, scanlM_eq_scanlM_toList, scanlM_empty, scanlM_pure, idRun_scanlM, List.toArray_scanlM, scanlM_extract, scanlM_map, toList_scanlM, Subarray.scanlM_eq_scanlM_extract
scanr 📖CompOp
18 mathmath: scanl_reverse, scanr_extract, back_scanr, idRun_scanrM, scanr_eq_scanrM, scanr_map, Subarray.scanr_eq_scanr_extract, size_scanr, back?_scanr, scanrM_pure, scanr_empty, scanr_eq_scanr_toList, scanr_push, List.toArray_scanr, getElem?_scanr_zero, toList_scanr, getElem_scanr_zero, getElem?_scanr
scanrM 📖CompOp
11 mathmath: scanrM_empty, scanlM_reverse, scanrM_map, idRun_scanrM, scanr_eq_scanrM, scanrM_eq_scanrM_toList, scanrM_pure, toList_scanrM, List.toArray_scanrM, Subarray.scanrM_eq_scanrM_extract, scanrM_extract
setN 📖CompOp

Array.scanlM

Definitions

NameCategoryTheorems
loop 📖CompOp
1 mathmath: loop_toList

Array.scanrM

Definitions

NameCategoryTheorems
loop 📖CompOp
1 mathmath: loop_toList

Subarray

Definitions

NameCategoryTheorems
contains 📖CompOp
isEmpty 📖CompOp
popHead? 📖CompOp
scanl 📖CompOp
1 mathmath: scanl_eq_scanl_extract
scanlM 📖CompOp
1 mathmath: scanlM_eq_scanlM_extract
scanr 📖CompOp
1 mathmath: scanr_eq_scanr_extract
scanrM 📖CompOp
1 mathmath: scanrM_eq_scanrM_extract

---

← Back to Index