Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `clamp`, `countP`, `dfoldl`, `dfoldlM`, `loop`, `dfoldr`, `dfoldrM`, `loop`, `divNat`, `find?`, `findRev?`, `findSome?`, `findSomeRev?`, `mkDivMod`, `modNat`, `prod`, `sum`	17
Theorems	0
Total	17

Fin

Definitions

Name	Category	Theorems
`clamp` 📖	CompOp	1 math math: `coe_clamp`
`countP` 📖	CompOp	5 math math: `countP_one`, `countP_succ`, `countP_eq_countP_map_finRange`, `countP_zero`, `countP_le`
`dfoldl` 📖	CompOp	5 math math: `dfoldl_eq_foldl`, `dfoldl_succ_last`, `dfoldl_succ`, `dfoldl_zero`, `dfoldl_eq_dfoldlM`
`dfoldlM` 📖	CompOp	4 math math: `dfoldlM_succ`, `dfoldl_eq_dfoldlM`, `dfoldlM_eq_foldlM`, `dfoldlM_zero`
`dfoldr` 📖	CompOp	5 math math: `dfoldr_eq_foldr`, `dfoldr_eq_dfoldrM`, `dfoldr_succ_last`, `dfoldr_succ`, `dfoldr_zero`
`dfoldrM` 📖	CompOp	4 math math: `dfoldr_eq_dfoldrM`, `dfoldrM_eq_foldrM`, `dfoldrM_zero`, `dfoldrM_succ`
`divNat` 📖	CompOp	3 math math: `divNat_mkDivMod_modNat`, `coe_divNat`, `divNat_mkDivMod`
`find?` 📖	CompOp	19 math math: `isSome_find?_iff`, `find?_one`, `find?_le_findRev?`, `map_rev_find?`, `find?_isNone_iff`, `find?_rev`, `find?_isSome_iff`, `bind_find?_isSome`, `find?_eq_some_iff`, `map_rev_findRev?`, `find?_eq_none_iff`, `find?_eq_findRev?_iff`, `findRev?_rev`, `find?_succ`, `find?_eq_find?_finRange`, `find?_zero`, `isSome_find?_of_eq_true`, `findSome?_guard`, `isNone_find?_iff`
`findRev?` 📖	CompOp	16 math math: `findRev?_one`, `findRev?_succ`, `find?_le_findRev?`, `map_rev_find?`, `findRev?_eq_none_iff`, `isSome_findRev?_iff`, `find?_rev`, `map_rev_findRev?`, `isSome_findRev?_of_eq_true`, `find?_eq_findRev?_iff`, `findRev?_rev`, `findRev?_zero`, `findSomeRev?_guard`, `bind_findRev?_isSome`, `isNone_findRev?_iff`, `findRev?_eq_some_iff`
`findSome?` 📖	CompOp	21 math math: `findSome?_eq_some_iff`, `findSome?_eq_none_iff`, `findSome?_zero`, `isSome_findSome?_of_isSome`, `map_findSome?`, `findSome?_succ_of_isSome`, `findSome?_isSome_iff`, `bind_find?_isSome`, `findSome?_succ_of_some`, `findSome?_rev`, `findSome?_eq_findSome?_finRange`, `findSome?_succ`, `findSome?_one`, `bind_findSome?_guard_isSome`, `findSome?_isNone_iff`, `findSome?_succ_of_none`, `findSomeRev?_rev`, `isNone_findSome?_iff`, `isSome_findSome?_iff`, `findSome?_succ_of_isNone`, `findSome?_guard`
`findSomeRev?` 📖	CompOp	14 math math: `findSomeRev?_eq_none_iff`, `map_findSomeRev?`, `findSomeRev?_eq_some_iff`, `bind_findSomeRev?_guard_isSome`, `findSome?_rev`, `findSomeRev?_succ`, `findSomeRev?_one`, `findSomeRev?_guard`, `isSome_findSomeRev?_of_isSome`, `isNone_findSomeRev?_iff`, `bind_findRev?_isSome`, `findSomeRev?_rev`, `isSome_findSomeRev?_iff`, `findSomeRev?_zero`
`mkDivMod` 📖	CompOp	4 math math: `divNat_mkDivMod_modNat`, `modNat_mkDivMod`, `divNat_mkDivMod`, `coe_mkDivMod`
`modNat` 📖	CompOp	3 math math: `divNat_mkDivMod_modNat`, `modNat_mkDivMod`, `coe_modNat`
`prod` 📖	CompOp	3 math math: `prod_succ`, `prod_zero`, `prod_eq_prod_map_finRange`
`sum` 📖	CompOp	3 math math: `sum_succ`, `sum_eq_sum_map_finRange`, `sum_zero`

Fin.dfoldlM

Definitions

Name	Category	Theorems
`loop` 📖	CompOp	3 math math: `Fin.dfoldlM_loop_lt`, `Fin.dfoldlM_loop_eq`, `Fin.dfoldlM_loop`

Fin.dfoldrM

Definitions

Name	Category	Theorems
`loop` 📖	CompOp	3 math math: `Fin.dfoldrM_loop`, `Fin.dfoldrM_loop_zero`, `Fin.dfoldrM_loop_succ`

---

← Back to Index