Add new functions to List module in basis

CakeML · May 5, 2023 · db4a478 · db4a478
1 parent 0523164
commit db4a478
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 0 deletions.
diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml
@@ -27,10 +27,19 @@ val res = translate LENGTH_AUX_THM;
 
 val _ = ml_prog_update open_local_block;
 val res = translate REV_DEF;
+val res = translate map_rev'_def;
+val res = translate filter_rev'_def;
+val res = translate flat_rev'_def;
 val _ = ml_prog_update open_local_in_block;
 
 val result = next_ml_names := ["rev"];
 val res = translate REVERSE_REV;
+val result = next_ml_names := ["mapRev"];
+val res = translate map_rev_def;
+val result = next_ml_names := ["filterRev"];
+val res = translate filter_rev_def;
+val result = next_ml_names := ["flatRev"];
+val res = translate flat_rev_def;
 
 (* New list-append translation *)
 val append_v_thm = trans "@" listSyntax.append_tm;

diff --git a/basis/types.txt b/basis/types.txt
@@ -19,6 +19,9 @@ Option.compare: ('a -> 'b -> ordering) -> 'a option -> 'b option -> ordering
 List.null: 'a list -> bool
 List.length: 'a list -> int
 List.rev: 'a list -> 'a list
+List.mapRev: ('a -> 'b) -> 'a list -> 'b list
+List.filterRev: ('a -> bool) -> 'a list -> 'a list
+List.flatRev: 'a list list -> 'a list
 List.@: 'a list -> 'a list -> 'a list
 List.hd: 'a list -> 'a
 List.tl: 'a list -> 'a list