diff --git a/src/core/CCVector.ml b/src/core/CCVector.ml index 40296609..240774fe 100644 --- a/src/core/CCVector.ml +++ b/src/core/CCVector.ml @@ -226,6 +226,20 @@ let append_list a b = match b with length v = List.length l1 + List.length l2) *) +let rec append_gen a b = match b() with + | None -> () + | Some x -> push a x; append_gen a b + +(*$Q + Q.(pair (list int)(list int)) (fun (l1,l2) -> \ + let v = of_list l1 in append_gen v (Gen.of_list l2); \ + to_list v = (l1 @ l2)) + Q.(pair (list int)(list int)) (fun (l1,l2) -> \ + let v = of_list l1 in append_gen v (Gen.of_list l2); \ + length v = List.length l1 + List.length l2) +*) + + (*$inject let gen x = let small = length in diff --git a/src/core/CCVector.mli b/src/core/CCVector.mli index e3a329cd..11dfdee6 100644 --- a/src/core/CCVector.mli +++ b/src/core/CCVector.mli @@ -84,6 +84,10 @@ val append_list : ('a, rw) t -> 'a list -> unit (** Append content of list @since 0.14 *) +val append_gen : ('a, rw) t -> 'a gen -> unit +(** Append content of generator + @since NEXT_RELEASE *) + val equal : 'a equal -> ('a,_) t equal val compare : 'a ord -> ('a,_) t ord