--- a/src/Pure/library.ML Sat Sep 04 21:45:43 2021 +0200
+++ b/src/Pure/library.ML Sat Sep 04 22:05:35 2021 +0200
@@ -51,6 +51,8 @@
val forall: ('a -> bool) -> 'a list -> bool
(*lists*)
+ val build: ('a list -> 'a list) -> 'a list
+ val build_rev: ('a list -> 'a list) -> 'a list
val single: 'a -> 'a list
val the_single: 'a list -> 'a
val singleton: ('a list -> 'b list) -> 'a -> 'b
@@ -301,6 +303,9 @@
(** lists **)
+fun build (f: 'a list -> 'a list) = f [];
+fun build_rev f = build f |> rev;
+
fun single x = [x];
fun the_single [x] = x