Commit 2023-07-07 11:12 7e1b24fa

View on Github →

refactor(Init.Data.List.Instances): sync to Mathlib 3 (#5751)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.bind_assoc

deleted theorem List.bind_singleton'

deleted theorem List.bind_singleton

deleted theorem List.map_eq_bind

Modified Mathlib/Init/Data/List/Instances.lean

added theorem List.bind_assoc

added theorem List.bind_singleton'

added theorem List.bind_singleton

added theorem List.map_eq_bind