Commit 2023-02-11 08:36 79ee3100

View on Github →

feat: port Data.List.Indexes (#1812)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Indexes.lean

added theorem List.findIdxs_eq_map_indexesValues

added theorem List.foldlIdxM_eq_foldlM_enum

added def List.foldlIdxSpec

added theorem List.foldlIdxSpec_cons

added theorem List.foldlIdx_eq_foldlIdxSpec

added theorem List.foldlIdx_eq_foldl_enum

added theorem List.foldrIdxM_eq_foldrM_enum

added def List.foldrIdxSpec

added theorem List.foldrIdxSpec_cons

added theorem List.foldrIdx_eq_foldrIdxSpec

added theorem List.foldrIdx_eq_foldr_enum

added theorem List.indexesValues_eq_filter_enum

added theorem List.length_mapIdx

added theorem List.list_reverse_induction

added theorem List.mapIdxGo_append

added theorem List.mapIdxGo_length

added theorem List.mapIdxM'_eq_mapIdxM

added theorem List.mapIdxMAux'_eq_mapIdxMGo

added def List.mapIdxMAuxSpec

added theorem List.mapIdxMAuxSpec_cons

added theorem List.mapIdxMGo_eq_mapIdxMAuxSpec

added theorem List.mapIdxM_eq_mmap_enum

added theorem List.mapIdx_append

added theorem List.mapIdx_append_one

added theorem List.mapIdx_cons

added theorem List.mapIdx_eq_enum_map

added theorem List.mapIdx_eq_ofFn

added theorem List.mapIdx_nil

added theorem List.map_enumFrom_eq_zipWith

added theorem List.nthLe_mapIdx