Fold

📁 Source: Batteries/Data/Fin/Fold.lean

Statistics

Metric	Count
Definitions	0
Theorems dfoldlM_eq_foldlM, dfoldlM_loop, dfoldlM_loop_eq, dfoldlM_loop_lt, dfoldlM_succ, dfoldlM_zero, dfoldl_eq_dfoldlM, dfoldl_eq_foldl, dfoldl_succ, dfoldl_succ_last, dfoldl_zero, dfoldrM_eq_foldrM, dfoldrM_loop, dfoldrM_loop_succ, dfoldrM_loop_zero, dfoldrM_succ, dfoldrM_zero, dfoldr_eq_dfoldrM, dfoldr_eq_foldr, dfoldr_succ, dfoldr_succ_last, dfoldr_zero, foldl_eq_foldl_finRange, foldr_eq_foldr_finRange	24
Total	24

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dfoldlM_eq_foldlM 📖	mathematical	—	dfoldlM	—	dfoldlM_zero dfoldlM_succ
dfoldlM_loop 📖	mathematical	—	dfoldlM.loop	—	—
dfoldlM_loop_eq 📖	mathematical	—	dfoldlM.loop	—	dfoldlM.loop.eq_1
dfoldlM_loop_lt 📖	mathematical	—	dfoldlM.loop	—	dfoldlM.loop.eq_1
dfoldlM_succ 📖	mathematical	—	dfoldlM	—	dfoldlM_loop
dfoldlM_zero 📖	mathematical	—	dfoldlM	—	dfoldlM.loop.eq_1
dfoldl_eq_dfoldlM 📖	mathematical	—	dfoldl dfoldlM	—	—
dfoldl_eq_foldl 📖	mathematical	—	dfoldl	—	dfoldl_zero dfoldl_succ
dfoldl_succ 📖	mathematical	—	dfoldl	—	dfoldlM_succ
dfoldl_succ_last 📖	mathematical	—	dfoldl	—	dfoldl_succ dfoldl_zero
dfoldl_zero 📖	mathematical	—	dfoldl	—	dfoldlM_zero
dfoldrM_eq_foldrM 📖	mathematical	—	dfoldrM	—	dfoldrM_succ
dfoldrM_loop 📖	mathematical	—	dfoldrM.loop	—	dfoldrM_loop_zero dfoldrM_loop_succ
dfoldrM_loop_succ 📖	mathematical	—	dfoldrM.loop	—	—
dfoldrM_loop_zero 📖	mathematical	—	dfoldrM.loop	—	—
dfoldrM_succ 📖	mathematical	—	dfoldrM	—	dfoldrM_loop
dfoldrM_zero 📖	mathematical	—	dfoldrM	—	—
dfoldr_eq_dfoldrM 📖	mathematical	—	dfoldr dfoldrM	—	—
dfoldr_eq_foldr 📖	mathematical	—	dfoldr	—	dfoldr_succ
dfoldr_succ 📖	mathematical	—	dfoldr	—	dfoldrM_succ
dfoldr_succ_last 📖	mathematical	—	dfoldr	—	dfoldr_succ
dfoldr_zero 📖	mathematical	—	dfoldr	—	—
foldl_eq_foldl_finRange 📖	—	—	—	—	—
foldr_eq_foldr_finRange 📖	—	—	—	—	—

---

← Back to Index