]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/extlib/hExtlib.mli
- hExtlib: new function "list_assoc_all"
[helm.git] / helm / software / components / extlib / hExtlib.mli
index 0a8921b1b83622298d107c9df1792cfa83a5d1b4..69843b235be58d541fe805265f7b1d8a91c47b4a 100644 (file)
@@ -119,6 +119,10 @@ val mk_list: 'a -> int -> 'a list
 
 (* makes the list [start; ...; stop - 1] *)
 val list_seq: int -> int -> int list
+
+(* like List.assoc but returns all bindings *)
+val list_assoc_all: 'a -> ('a * 'b) list -> 'b list
+
 (** {2 Debugging & Profiling} *)
 
 type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b }