Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-28 01:31 131b46f1

View on Github →

feat(data/list): separate out list defs into data.lists.defs

Estimated changes

Modified data/list/basic.lean

deleted inductive list.chain

deleted theorem list.chain_cons

deleted def list.choose

deleted def list.choose_x

deleted def list.concat

deleted def list.count

deleted def list.countp

deleted def list.disjoint

deleted def list.erase_dup

deleted def list.erasep

deleted def list.extractp

deleted def list.find

deleted def list.find_indexes

deleted def list.find_indexes_aux

deleted def list.head'

deleted def list.indexes_of

deleted def list.inits

deleted def list.insert_nth

deleted def list.inth

deleted def list.is_infix

deleted def list.is_prefix

deleted def list.is_suffix

deleted def list.last'

deleted def list.lookmap

deleted def list.map_head

deleted def list.map_last

deleted def list.modify_head

deleted def list.modify_nth

deleted def list.modify_nth_tail

deleted def list.nodup

deleted def list.of_fn

deleted def list.of_fn_aux

deleted def list.of_fn_nth_val

deleted inductive list.pairwise

deleted theorem list.pairwise_cons

deleted def list.permutations

deleted def list.permutations_aux.rec

deleted def list.permutations_aux2

deleted def list.permutations_aux

deleted def list.prod

deleted def list.product

deleted def list.pw_filter

deleted def list.range'

deleted def list.reduce_option

deleted def list.revzip

deleted def list.scanl

deleted def list.scanr

deleted def list.scanr_aux

deleted def list.sections

deleted def list.split_at

deleted def list.sublists'

deleted def list.sublists'_aux

deleted def list.sublists

deleted def list.sublists_aux

deleted def list.sublists_aux₁

deleted def list.tails

deleted def list.take'

deleted def list.take_while

deleted def list.tfae

deleted def list.to_array

deleted def list.transpose

deleted def list.transpose_aux

Created data/list/defs.lean

added inductive list.chain

added theorem list.chain_cons

added def list.choose

added def list.choose_x

added def list.concat

added def list.count

added def list.countp

added def list.disjoint

added def list.erase_dup

added def list.erasep

added def list.extractp

added def list.find

added def list.find_indexes

added def list.find_indexes_aux

added def list.head'

added def list.indexes_of

added def list.inits

added def list.insert_nth

added def list.inth

added def list.is_infix

added def list.is_prefix

added def list.is_suffix

added def list.last'

added def list.lookmap

added def list.map_head

added def list.map_last

added def list.modify_head

added def list.modify_nth

added def list.modify_nth_tail

added def list.nodup

added def list.of_fn

added def list.of_fn_aux

added def list.of_fn_nth_val

added inductive list.pairwise

added theorem list.pairwise_cons

added def list.permutations

added def list.permutations_aux.rec

added def list.permutations_aux2

added def list.permutations_aux

added def list.prod

added def list.product

added def list.pw_filter

added def list.range'

added def list.reduce_option

added def list.revzip

added def list.scanl

added def list.scanr

added def list.scanr_aux

added def list.sections

added def list.split_at

added def list.sublists'

added def list.sublists'_aux

added def list.sublists

added def list.sublists_aux

added def list.sublists_aux₁

added def list.tails

added def list.take'

added def list.take_while

added def list.tfae

added def list.to_array

added def list.transpose

added def list.transpose_aux