diff options
author | 1999-08-17 14:05:09 +0000 | |
---|---|---|
committer | 1999-08-17 14:05:09 +0000 | |
commit | 6b2bb43c4eb815af8f7128b2f2848157c6b020d7 (patch) | |
tree | 777100903d85aa79b5477feb05d2a9d397a9acc0 /lib/util.mli | |
parent | d269b37bdfed0adfdb3435b4e6715ae44267307d (diff) |
ajout dyn; divers fonctions util
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
-rw-r--r-- | lib/util.mli | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 5d4c706b9..4e92b46b8 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -25,6 +25,30 @@ val parse_section_path : string -> string list * string * string val intersect : 'a list -> 'a list -> 'a list val subtract : 'a list -> 'a list -> 'a list +(* Arrays *) + +val array_exists : ('a -> bool) -> 'a array -> bool +val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool +val array_hd : 'a array -> 'a +val array_tl : 'a array -> 'a array +val array_cons : 'a -> 'a array -> 'a array +val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a +val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b +val array_app_tl : 'a array -> 'a list -> 'a list +val array_list_of_tl : 'a array -> 'a list +val array_map_to_list : ('a -> 'b) -> 'a array ->'b list + +(* Functions *) + +val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b +val iterate : ('a -> 'a) -> int -> 'a -> 'a + +(* Misc *) + +type ('a,'b) union = Inl of 'a | Inr of 'b + +module Intset : Set.S with type elt = int + (* Pretty-printing *) val pr_spc : unit -> std_ppcmds |