Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-07 18:26 4e24f4cf

View on Github →

feat(data/list/*): add indexed versions of some list functions (#2191) Add foldr_with_index, foldl_with_index, mfoldr_with_index, mfoldl_with_index, mmap_with_index and mmap_with_index'. The new functions are proven correct by relating them to their non-indexed counterparts.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.filter_eq_foldr

added theorem list.map_eq_foldr

added theorem list.map_filter_eq_foldr

added theorem list.mfoldl_eq_foldl

added theorem list.mfoldr_eq_foldr

Modified src/data/list/default.lean

Modified src/data/list/defs.lean

added def list.foldl_with_index

added def list.foldl_with_index_aux

added def list.foldr_with_index

added def list.foldr_with_index_aux

modified def list.indexes_values

deleted def list.indexes_values_aux

added def list.mfoldl_with_index

added def list.mfoldr_with_index

added def list.mmap_with_index'

added def list.mmap_with_index'_aux

added def list.mmap_with_index

added def list.mmap_with_index_aux

Created src/data/list/indexes.lean

added theorem list.find_indexes_eq_map_indexes_values

added theorem list.foldl_with_index_aux_eq_foldl_with_index_aux_spec

added def list.foldl_with_index_aux_spec

added theorem list.foldl_with_index_aux_spec_cons

added theorem list.foldl_with_index_eq_foldl_enum

added theorem list.foldr_with_index_aux_eq_foldr_with_index_aux_spec

added def list.foldr_with_index_aux_spec

added theorem list.foldr_with_index_aux_spec_cons

added theorem list.foldr_with_index_eq_foldr_enum

added theorem list.indexes_values_eq_filter_enum

added theorem list.mfoldl_with_index_eq_mfoldl_enum

added theorem list.mfoldr_with_index_eq_mfoldr_enum

added theorem list.mmap_with_index'_aux_eq_mmap_with_index_aux

added theorem list.mmap_with_index'_eq_mmap_with_index

added theorem list.mmap_with_index_aux_eq_mmap_with_index_aux_spec

added def list.mmap_with_index_aux_spec

added theorem list.mmap_with_index_aux_spec_cons

added theorem list.mmap_with_index_eq_mmap_enum

Modified src/data/list/zip.lean

added theorem list.map_fst_zip

added theorem list.map_snd_zip