aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/cArray.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-05 15:38:43 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-05 15:38:43 +0000
commit38ac6e0eff49662636e8db6ceb5f4badbdc7795a (patch)
tree0a70704700ea171430eb9a4e532168a76603ae43 /lib/cArray.mli
parent407631d36ce77071556a80d6665cffc7d9a6c94a (diff)
Missing primitive in CArray
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/cArray.mli')
-rw-r--r--lib/cArray.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/cArray.mli b/lib/cArray.mli
index ed8a1e94c..0e0be1dfd 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -47,6 +47,9 @@ sig
val equal : ('a -> 'a -> bool) -> 'a array -> 'a array -> bool
(** Lift equality to array type. *)
+ val is_empty : 'a array -> bool
+ (** True whenever the array is empty. *)
+
val exists : ('a -> bool) -> 'a array -> bool
(** As [List.exists] but on arrays. *)