Commit 2025-02-12 18:57 8ca089fa

View on Github →

chore(Data/List/Basic): split take and drop from file (#21232) This PR splits Data/List/Basic.lean decls and lemmas related to take or drop into a new TakeDrop.lean file, decreasing the length of a file triggering the long file linter.

Estimated changes

deleted theorem List.cons_get_drop_succ
deleted theorem List.dropSlice_eq
deleted theorem List.drop_length_sub_one
deleted theorem List.left_eq_take_iff
deleted theorem List.length_dropSlice
deleted theorem List.length_dropSlice_lt
deleted theorem List.takeD_eq_take
deleted theorem List.takeD_left'
deleted theorem List.takeD_left
deleted theorem List.takeD_length
deleted theorem List.takeI_eq_take
deleted theorem List.takeI_left'
deleted theorem List.takeI_left
deleted theorem List.takeI_length
deleted theorem List.takeI_nil
deleted theorem List.take_concat_get'
deleted theorem List.take_eq_left_iff
deleted theorem List.take_eq_self_iff
deleted theorem List.take_self_eq_iff
added theorem List.dropSlice_eq
added theorem List.left_eq_take_iff
added theorem List.length_dropSlice
added theorem List.takeD_eq_take
added theorem List.takeD_left'
added theorem List.takeD_left
added theorem List.takeD_length
added theorem List.takeI_eq_take
added theorem List.takeI_left'
added theorem List.takeI_left
added theorem List.takeI_length
added theorem List.takeI_nil
added theorem List.take_concat_get'
added theorem List.take_eq_left_iff
added theorem List.take_eq_self_iff
added theorem List.take_self_eq_iff