Commit 2024-03-26 14:16 9d4c1bc6

View on Github →

chore(List): deprecate List.ret (#11651) Use List.pure from Lean core instead.

Estimated changes

Modified Mathlib/Computability/Encoding.lean

modified theorem Computability.decode_encodeBool

modified def Computability.encodeBool

Modified Mathlib/Data/List/Basic.lean

added theorem List.bind_pure_eq_map

modified theorem List.bind_ret_eq_map

modified theorem List.mem_pure

Modified Mathlib/Data/List/Sublists.lean

added theorem List.map_pure_sublist_sublists

modified theorem List.map_ret_sublist_sublists

Modified Mathlib/Data/Multiset/Powerset.lean

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

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

added theorem List.pure_def