--- a/src/Pure/General/vector.ML Fri Apr 14 22:55:01 2023 +0200
+++ b/src/Pure/General/vector.ML Sat Apr 15 13:51:38 2023 +0200
@@ -9,6 +9,7 @@
include VECTOR
val nth: 'a vector -> int -> 'a
val forall: ('a -> bool) -> 'a vector -> bool
+ val member: ('a * 'a -> bool) -> 'a vector -> 'a -> bool
val fold: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
val fold_rev: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
end;
@@ -22,6 +23,8 @@
val forall = all;
+fun member eq vec x = exists (fn y => eq (x, y)) vec;
+
fun fold f vec x = foldl (fn (a, b) => f a b) x vec;
fun fold_rev f vec x = foldr (fn (a, b) => f a b) x vec;