Documentation Verification Report

Scan

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

Statistics

MetricCount
Definitions0
Theoremsdrop_scanr, getElem?_partialProds, getElem?_partialSums, getElem?_scanl, getElem?_scanl_zero, getElem?_scanr, getElem?_scanr_of_lt, getElem?_scanr_zero, getElem?_succ_scanl, getElem_flatten, getElem_flatten_aux₁, getElem_flatten_aux₂, getElem_partialProds, getElem_partialSums, getElem_scanl, getElem_scanl_zero, getElem_scanr, getElem_scanr_zero, getElem_succ_scanl, getLast?_scanl, getLast?_scanr, getLast_scanl, getLast_scanr, head_scanl, head_scanr, idRun_scanlM, idRun_scanrM, length_flatten_mem_partialSums_map_length, length_partialProds, length_partialSums, length_scanl, length_scanr, partialProds_append, partialProds_cons, partialProds_nil, partialSums_append, partialSums_cons, partialSums_ne_nil, partialSums_nil, go_eq_append_map, scanAuxM_cons, scanAuxM_nil, scanlM_cons, scanlM_eq_scanrM_reverse, scanlM_map, scanlM_nil, scanlM_pure, scanlM_reverse, scanl_append, scanl_cons, scanl_eq_scanr_reverse, scanl_eq_singleton_iff, scanl_map, scanl_ne_nil, scanl_nil, scanl_reverse, scanl_singleton, scanrM_concat, scanrM_eq_scanlM_reverse, scanrM_map, scanrM_nil, scanrM_pure, scanrM_reverse, scanr_append, scanr_cons, scanr_eq_scanl_reverse, scanr_iff_nil, scanr_map, scanr_ne_nil, scanr_nil, scanr_reverse, scanr_singleton, tail_scanl, tail_scanr, take_partialProds, take_partialSums, take_scanl
77
Total77

List

Theorems

NameKindAssumesProvesValidatesDepends On
drop_scanr 📖mathematicalscanr
getElem?_partialProds 📖mathematicalpartialProds
prod
getElem?_partialSums 📖mathematicalpartialSums
getElem?_scanl 📖mathematicalscanl
getElem?_scanl_zero 📖mathematicalscanllength_scanl
getElem_scanl
getElem?_scanr 📖mathematicalscanr
getElem?_scanr_of_lt 📖mathematicalscanrlength_scanr
getElem_scanr
getElem?_scanr_zero 📖mathematicalscanrlength_scanr
getElem_scanr
getElem?_succ_scanl 📖mathematicalscanl
getElem_flatten 📖getElem_flatten_aux₁
getElem_flatten_aux₂
partialSums_cons
getElem_partialSums
length_partialSums
getElem_flatten_aux₁ 📖mathematicalpartialSumsgetElem_partialSums
length_partialSums
length_flatten_mem_partialSums_map_length
getElem_flatten_aux₂ 📖mathematicalpartialSums
getElem_flatten_aux₁
getElem_flatten_aux₁
partialSums_cons
length_partialSums
getElem_partialSums
getElem_partialProds 📖mathematicalpartialProdsprodgetElem_scanl
prod_eq_foldl
getElem_partialSums 📖partialSumsgetElem_scanl
sum_eq_foldl
getElem_scanl 📖scanl
getElem_scanl_zero 📖mathematicalscanlgetElem_scanl
getElem_scanr 📖scanr
getElem_scanr_zero 📖mathematicalscanrgetElem_scanr
getElem_succ_scanl 📖scanl
getLast?_scanl 📖mathematicalscanl
getLast?_scanr 📖mathematicalscanr
getLast_scanl 📖mathematicalscanl
getLast_scanr 📖mathematicalscanr
head_scanl 📖mathematicalscanl
head_scanr 📖mathematicalscanr
idRun_scanlM 📖mathematicalscanlM
scanl
scanlM_pure
idRun_scanrM 📖mathematicalscanrM
scanr
scanrM_pure
length_flatten_mem_partialSums_map_length 📖mathematicalpartialSumspartialSums_nil
partialSums_cons
length_partialProds 📖mathematicalpartialProdslength_scanl
length_partialSums 📖mathematicalpartialSumslength_scanl
length_scanl 📖mathematicalscanlscanlM_nil
scanlM_cons
length_scanr 📖mathematicalscanrscanr_nil
scanr_cons
partialProds_append 📖mathematicalpartialProds
prod
scanl_nil
scanl_cons
partialProds_cons
partialProds_cons 📖mathematicalpartialProdsscanl_cons
scanl_nil
partialProds_nil 📖mathematicalpartialProdsscanl_nil
partialSums_append 📖mathematicalpartialSumsscanl_nil
scanl_cons
partialSums_cons
partialSums_cons 📖mathematicalpartialSumsscanl_cons
scanl_nil
partialSums_ne_nil 📖length_partialSums
partialSums_nil 📖mathematicalpartialSumsscanl_nil
scanAuxM_cons 📖mathematicalscanAuxMscanAuxM.eq_1
scanAuxM.go.eq_2
scanAuxM.go_eq_append_map
scanAuxM_nil 📖mathematicalscanAuxM
scanlM_cons 📖mathematicalscanlMscanAuxM_cons
scanlM_eq_scanrM_reverse 📖mathematicalscanlM
scanrM
scanlM_map 📖mathematicalscanlM
scanlM_nil 📖mathematicalscanlM
scanlM_pure 📖mathematicalscanlM
scanl
scanlM_nil
scanlM_cons
scanlM_reverse 📖mathematicalscanlM
scanrM
scanlM_eq_scanrM_reverse
scanl_append 📖mathematicalscanlscanl_nil
scanl_cons
scanl_cons 📖mathematicalscanlscanlM_cons
scanl_eq_scanr_reverse 📖mathematicalscanl
scanr
scanrM_reverse
scanl_eq_singleton_iff 📖mathematicalscanl
scanl_map 📖mathematicalscanl
scanl_ne_nil 📖scanl_nil
scanl_cons
scanl_nil 📖mathematicalscanlscanlM_nil
scanl_reverse 📖mathematicalscanl
scanr
scanl_nil
scanr_nil
scanl_append
scanl_cons
scanr_cons
scanl_singleton 📖mathematicalscanlscanl_cons
scanl_nil
scanrM_concat 📖mathematicalscanrMscanAuxM_cons
scanrM_eq_scanlM_reverse 📖mathematicalscanrM
scanlM
scanlM_eq_scanrM_reverse
scanrM_map 📖mathematicalscanrMscanrM_eq_scanlM_reverse
scanlM_map
scanrM_nil 📖mathematicalscanrM
scanrM_pure 📖mathematicalscanrM
scanr
scanrM_eq_scanlM_reverse
scanlM_pure
scanrM_reverse 📖mathematicalscanrM
scanlM
scanrM_eq_scanlM_reverse
scanr_append 📖mathematicalscanrscanr_nil
scanr_cons
scanr_cons 📖mathematicalscanrscanr_eq_scanl_reverse
scanl_append
scanl_cons
scanl_nil
scanr_eq_scanl_reverse 📖mathematicalscanr
scanl
scanl_eq_scanr_reverse
scanr_iff_nil 📖mathematicalscanr
scanr_map 📖mathematicalscanrscanr_nil
scanr_cons
scanr_ne_nil 📖scanr_nil
scanr_cons
scanr_nil 📖mathematicalscanr
scanr_reverse 📖mathematicalscanr
scanl
scanr_append
scanr_cons
scanr_nil
scanl_cons
scanr_singleton 📖mathematicalscanrscanr_cons
scanr_nil
tail_scanl 📖mathematicalscanl
tail_scanr 📖mathematicalscanrscanr_cons
take_partialProds 📖mathematicalpartialProdstake_scanl
take_partialSums 📖mathematicalpartialSumstake_scanl
take_scanl 📖mathematicalscanl

List.scanAuxM

Theorems

NameKindAssumesProvesValidatesDepends On
go_eq_append_map 📖mathematicalgo
List.scanAuxM

---

← Back to Index