From 0fe99a0d6a4d643cf311200c870aeaff042d7069 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Thu, 16 Jan 2020 13:28:28 +0100 Subject: replace RList by list R add an overlay for coquelicot remove functions from RList: In, Rlength, cons_Rlist, app_RList because they are essentially the same as In, length, app, and map from List (beware that the order of arguments changes for map, and the In function contains reversed equalities). adds deprecation warnings for Rlist and Rlength adds deprecated notations for RList.cons and RList.nil --- doc/changelog/10-standard-library/11404-removeRList.rst | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 doc/changelog/10-standard-library/11404-removeRList.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst new file mode 100644 index 0000000000..88e22d128c --- /dev/null +++ b/doc/changelog/10-standard-library/11404-removeRList.rst @@ -0,0 +1,15 @@ +- **Removed:** + Type `RList` has been removed. All uses have been replaced by `list R`. + Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist` + have also been removed as they are essentially the same as `In`, `length`, + `app`, and `map` from `List`, modulo the following changes: + + - `RList.In x (RList.cons a l)` used to be convertible to + `(x = a) \\/ RList.In x l`, + but `List.In x (a :: l)` is convertible to + `(a = x) \\/ List.In l`. + The equality is reversed. + - `app_Rlist` and `List.map` take arguments in different order. + + (`#11404 `_, + by Yves Bertot). -- cgit v1.2.3