Commit 2024-03-26 14:16 5cc0a412

View on Github →

chore(List/ReduceOption): move from Basic.lean (#11662) Also rename List.IsPrefix.filter_map to List.IsPrefix.filterMap and protect some theorems in the List.IsPrefix namespace.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.reduceOption_append

deleted theorem List.reduceOption_concat

deleted theorem List.reduceOption_concat_of_some

deleted theorem List.reduceOption_cons_of_none

deleted theorem List.reduceOption_cons_of_some

deleted theorem List.reduceOption_get?_iff

deleted theorem List.reduceOption_length_eq_iff

deleted theorem List.reduceOption_length_le

deleted theorem List.reduceOption_length_lt_iff

deleted theorem List.reduceOption_map

deleted theorem List.reduceOption_mem_iff

deleted theorem List.reduceOption_nil

deleted theorem List.reduceOption_singleton

Modified Mathlib/Data/List/Infix.lean

deleted theorem List.IsPrefix.filter_map

deleted theorem List.IsPrefix.map

deleted theorem List.IsPrefix.reduceOption

Created Mathlib/Data/List/ReduceOption.lean

added theorem List.reduceOption_append

added theorem List.reduceOption_concat

added theorem List.reduceOption_concat_of_some

added theorem List.reduceOption_cons_of_none

added theorem List.reduceOption_cons_of_some

added theorem List.reduceOption_get?_iff

added theorem List.reduceOption_length_eq_iff

added theorem List.reduceOption_length_le

added theorem List.reduceOption_length_lt_iff

added theorem List.reduceOption_map

added theorem List.reduceOption_mem_iff

added theorem List.reduceOption_nil

added theorem List.reduceOption_singleton