Scan

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

Statistics

Metric	Count
Definitions	0
Theorems `back?_scanr`, `back_scanl`, `back_scanl?`, `back_scanr`, `getElem?_scanl`, `getElem?_scanl_zero`, `getElem?_scanr`, `getElem?_scanr_zero`, `getElem?_succ_scanl`, `getElem_scanl`, `getElem_scanl_zero`, `getElem_scanr`, `getElem_scanr_zero`, `getElem_succ_scanl`, `idRun_scanlM`, `idRun_scanrM`, `loop_toList`, `scanlM_empty`, `scanlM_eq_scanlM_toList`, `scanlM_extract`, `scanlM_map`, `scanlM_pure`, `scanlM_reverse`, `scanl_empty`, `scanl_eq_scanlM`, `scanl_eq_scanl_toList`, `scanl_eq_singleton_iff`, `scanl_extract`, `scanl_map`, `scanl_ne_empty`, `scanl_push`, `scanl_reverse`, `scanl_singleton`, `loop_toList`, `scanrM_empty`, `scanrM_eq_scanrM_toList`, `scanrM_extract`, `scanrM_map`, `scanrM_pure`, `scanr_empty`, `scanr_eq_scanrM`, `scanr_eq_scanr_toList`, `scanr_extract`, `scanr_map`, `scanr_ne_empty`, `scanr_push`, `size_scanl`, `size_scanr`, `take_scanl`, `toList_scanl`, `toList_scanlM`, `toList_scanr`, `toList_scanrM`, `toArray_scanl`, `toArray_scanlM`, `toArray_scanr`, `toArray_scanrM`, `scanlM_eq_scanlM_extract`, `scanl_eq_scanl_extract`, `scanrM_eq_scanrM_extract`, `scanr_eq_scanr_extract`	61
Total	61

Array

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`back?_scanr` 📖	mathematical	—	`scanr`	—	`toList_scanr` `List.getLast?_scanr`
`back_scanl` 📖	mathematical	—	`scanl`	—	`size_scanl` `getElem_scanl`
`back_scanl?` 📖	mathematical	—	`scanl`	—	`size_scanl` `getElem_scanl`
`back_scanr` 📖	mathematical	—	`scanr`	—	`toList_scanr` `List.getLast_scanr`
`getElem?_scanl` 📖	mathematical	—	`scanl`	—	—
`getElem?_scanl_zero` 📖	mathematical	—	`scanl`	—	`size_scanl` `getElem_scanl` `extract_empty_of_start_eq_stop`
`getElem?_scanr` 📖	mathematical	—	`scanr`	—	—
`getElem?_scanr_zero` 📖	mathematical	—	`scanr`	—	`size_scanr` `getElem_scanr`
`getElem?_succ_scanl` 📖	mathematical	—	`scanl`	—	`scanl_eq_scanl_toList` `List.getElem?_succ_scanl`
`getElem_scanl` 📖	—	`scanl`	—	—	`scanl_eq_scanl_toList` `List.getElem_scanl`
`getElem_scanl_zero` 📖	mathematical	—	`scanl`	—	`getElem_scanl` `extract_empty_of_start_eq_stop`
`getElem_scanr` 📖	—	`scanr`	—	—	`scanr_eq_scanr_toList`
`getElem_scanr_zero` 📖	mathematical	—	`scanr`	—	`getElem_scanr`
`getElem_succ_scanl` 📖	—	`scanl`	—	—	`scanl_eq_scanl_toList`
`idRun_scanlM` 📖	mathematical	—	`scanlM` `scanl`	—	`scanlM_pure`
`idRun_scanrM` 📖	mathematical	—	`scanrM` `scanr`	—	`scanrM_pure`
`scanlM_empty` 📖	mathematical	—	`scanlM`	—	`scanlM.loop.congr_simp` `scanlM.loop.eq_1`
`scanlM_eq_scanlM_toList` 📖	mathematical	—	`scanlM` `List.scanlM`	—	`scanlM.loop.congr_simp` `scanlM.loop_toList`
`scanlM_extract` 📖	mathematical	—	`scanlM`	—	`scanlM.eq_1` `scanlM.loop_toList` `scanlM_eq_scanlM_toList`
`scanlM_map` 📖	mathematical	—	`scanlM`	—	`scanlM_eq_scanlM_toList` `List.scanlM_map`
`scanlM_pure` 📖	mathematical	—	`scanlM` `scanl`	—	`scanlM_eq_scanlM_toList` `List.scanlM_pure`
`scanlM_reverse` 📖	mathematical	—	`scanlM` `scanrM`	—	`scanlM_eq_scanlM_toList` `scanrM_eq_scanrM_toList` `List.scanlM_reverse`
`scanl_empty` 📖	mathematical	—	`scanl`	—	—
`scanl_eq_scanlM` 📖	mathematical	—	`scanl` `scanlM`	—	`scanlM_pure`
`scanl_eq_scanl_toList` 📖	mathematical	—	`scanl` `List.scanl`	—	`scanl_eq_scanlM` `scanlM_eq_scanlM_toList`
`scanl_eq_singleton_iff` 📖	mathematical	—	`scanl`	—	—
`scanl_extract` 📖	mathematical	—	`scanl`	—	`scanlM_extract`
`scanl_map` 📖	mathematical	—	`scanl`	—	`scanl_eq_scanl_toList` `List.scanl_map`
`scanl_ne_empty` 📖	—	—	—	—	—
`scanl_push` 📖	mathematical	—	`scanl`	—	`scanl_eq_scanl_toList` `List.scanl_append` `List.scanl_cons` `List.scanl_nil`
`scanl_reverse` 📖	mathematical	—	`scanl` `scanr`	—	`scanl_eq_scanl_toList` `scanr_eq_scanr_toList` `List.scanl_reverse`
`scanl_singleton` 📖	mathematical	—	`scanl`	—	—
`scanrM_empty` 📖	mathematical	—	`scanrM`	—	`scanrM.loop.congr_simp` `scanrM.loop.eq_1`
`scanrM_eq_scanrM_toList` 📖	mathematical	—	`scanrM` `List.scanrM`	—	`scanrM.loop.congr_simp` `scanrM.loop_toList`
`scanrM_extract` 📖	mathematical	—	`scanrM`	—	`scanrM.eq_1` `scanrM.loop_toList` `scanrM_eq_scanrM_toList`
`scanrM_map` 📖	mathematical	—	`scanrM`	—	`scanrM_eq_scanrM_toList` `List.scanrM_map`
`scanrM_pure` 📖	mathematical	—	`scanrM` `scanr`	—	`scanrM_eq_scanrM_toList` `List.scanrM_pure`
`scanr_empty` 📖	mathematical	—	`scanr`	—	—
`scanr_eq_scanrM` 📖	mathematical	—	`scanr` `scanrM`	—	`scanrM_pure`
`scanr_eq_scanr_toList` 📖	mathematical	—	`scanr` `List.scanr`	—	`scanr_eq_scanrM` `scanrM_eq_scanrM_toList`
`scanr_extract` 📖	mathematical	—	`scanr`	—	`scanrM_extract`
`scanr_map` 📖	mathematical	—	`scanr`	—	`scanr_eq_scanr_toList` `List.scanr_map`
`scanr_ne_empty` 📖	—	—	—	—	—
`scanr_push` 📖	mathematical	—	`scanr`	—	—
`size_scanl` 📖	mathematical	—	`scanl`	—	—
`size_scanr` 📖	mathematical	—	`scanr`	—	—
`take_scanl` 📖	mathematical	—	`scanl`	—	—
`toList_scanl` 📖	mathematical	—	`scanl` `List.scanl`	—	`scanl_eq_scanl_toList`
`toList_scanlM` 📖	mathematical	—	`scanlM` `List.scanlM`	—	`scanlM_eq_scanlM_toList`
`toList_scanr` 📖	mathematical	—	`scanr` `List.scanr`	—	`scanr_eq_scanr_toList`
`toList_scanrM` 📖	mathematical	—	`scanrM` `List.scanrM`	—	`scanrM_eq_scanrM_toList`

Array.scanlM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`loop_toList` 📖	mathematical	—	`loop` `List.scanlM`	—	`loop.eq_def` `List.scanlM_nil` `List.scanlM_cons`

Array.scanrM

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`loop_toList` 📖	mathematical	—	`loop` `List.scanrM`	—	`loop.eq_1` `loop.eq_def` `List.scanrM_eq_scanlM_reverse` `List.take_succ_drop` `List.scanlM_cons` `List.scanlM_reverse`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toArray_scanl` 📖	mathematical	—	`scanl` `Array.scanl`	—	`Array.toList_scanl`
`toArray_scanlM` 📖	mathematical	—	`scanlM` `Array.scanlM`	—	`Array.toList_scanlM`
`toArray_scanr` 📖	mathematical	—	`scanr` `Array.scanr`	—	`Array.toList_scanr`
`toArray_scanrM` 📖	mathematical	—	`scanrM` `Array.scanrM`	—	`Array.toList_scanrM`

Subarray

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`scanlM_eq_scanlM_extract` 📖	mathematical	—	`scanlM` `Array.scanlM`	—	`Array.scanlM_extract`
`scanl_eq_scanl_extract` 📖	mathematical	—	`scanl` `Array.scanl`	—	`Array.scanl_extract`
`scanrM_eq_scanrM_extract` 📖	mathematical	—	`scanrM` `Array.scanrM`	—	`Array.scanrM_extract`
`scanr_eq_scanr_extract` 📖	mathematical	—	`scanr` `Array.scanr`	—	`Array.scanr_extract`

---

← Back to Index