Commit 2021-05-30 21:09 fd48ac55

View on Github →

chore(data/list): extract sublists to a separate file (#7757) Minor splitting in data/list/basic, splitting out sublists to its own file, thereby delaying importing data.nat.choose in the list development.

Estimated changes

Modified src/data/list/basic.lean

deleted theorem list.length_of_sublists_len

deleted theorem list.length_sublists'

deleted theorem list.length_sublists

deleted theorem list.length_sublists_len

deleted theorem list.map_ret_sublist_sublists

deleted theorem list.map_sublists'_aux

deleted theorem list.mem_sublists'

deleted theorem list.mem_sublists

deleted theorem list.mem_sublists_len

deleted theorem list.mem_sublists_len_self

deleted theorem list.sublists'_aux_append

deleted theorem list.sublists'_aux_eq_sublists'

deleted theorem list.sublists'_cons

deleted theorem list.sublists'_eq_sublists

deleted theorem list.sublists'_nil

deleted theorem list.sublists'_reverse

deleted theorem list.sublists'_singleton

deleted theorem list.sublists_append

deleted theorem list.sublists_aux_cons_append

deleted theorem list.sublists_aux_cons_cons

deleted theorem list.sublists_aux_cons_eq_sublists_aux₁

deleted theorem list.sublists_aux_eq_foldr.aux

deleted theorem list.sublists_aux_eq_foldr

deleted theorem list.sublists_aux_ne_nil

deleted theorem list.sublists_aux₁_append

deleted theorem list.sublists_aux₁_bind

deleted theorem list.sublists_aux₁_concat

deleted theorem list.sublists_aux₁_eq_sublists_aux

deleted theorem list.sublists_concat

deleted theorem list.sublists_eq_sublists'

deleted def list.sublists_len

deleted def list.sublists_len_aux

deleted theorem list.sublists_len_aux_append

deleted theorem list.sublists_len_aux_eq

deleted theorem list.sublists_len_aux_zero

deleted theorem list.sublists_len_sublist_of_sublist

deleted theorem list.sublists_len_sublist_sublists'

deleted theorem list.sublists_len_succ_cons

deleted theorem list.sublists_len_succ_nil

deleted theorem list.sublists_len_zero

deleted theorem list.sublists_nil

deleted theorem list.sublists_reverse

deleted theorem list.sublists_singleton

Modified src/data/list/pairwise.lean

Created src/data/list/sublists.lean

added theorem list.length_of_sublists_len

added theorem list.length_sublists'

added theorem list.length_sublists

added theorem list.length_sublists_len

added theorem list.map_ret_sublist_sublists

added theorem list.map_sublists'_aux

added theorem list.mem_sublists'

added theorem list.mem_sublists

added theorem list.mem_sublists_len

added theorem list.mem_sublists_len_self

added theorem list.sublists'_aux_append

added theorem list.sublists'_aux_eq_sublists'

added theorem list.sublists'_cons

added theorem list.sublists'_eq_sublists

added theorem list.sublists'_nil

added theorem list.sublists'_reverse

added theorem list.sublists'_singleton

added theorem list.sublists_append

added theorem list.sublists_aux_cons_append

added theorem list.sublists_aux_cons_cons

added theorem list.sublists_aux_cons_eq_sublists_aux₁

added theorem list.sublists_aux_eq_foldr.aux

added theorem list.sublists_aux_eq_foldr

added theorem list.sublists_aux_ne_nil

added theorem list.sublists_aux₁_append

added theorem list.sublists_aux₁_bind

added theorem list.sublists_aux₁_concat

added theorem list.sublists_aux₁_eq_sublists_aux

added theorem list.sublists_concat

added theorem list.sublists_eq_sublists'

added def list.sublists_len

added def list.sublists_len_aux

added theorem list.sublists_len_aux_append

added theorem list.sublists_len_aux_eq

added theorem list.sublists_len_aux_zero

added theorem list.sublists_len_sublist_of_sublist

added theorem list.sublists_len_sublist_sublists'

added theorem list.sublists_len_succ_cons

added theorem list.sublists_len_succ_nil

added theorem list.sublists_len_zero

added theorem list.sublists_nil

added theorem list.sublists_reverse

added theorem list.sublists_singleton