X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fextlib%2FhExtlib.ml;h=3ef795e9fca4badc9299cd2a0f4207fe1af2afa5;hb=6b3242efcd29ea188ef09b445985abb06c5fad3a;hp=3fe5c0a7d40762ba0340a82ddad0dc685ee1c44c;hpb=8d58fba703fcb1cfddd2a78a0b157a087bcf2a5b;p=helm.git diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index 3fe5c0a7d..3ef795e9f 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -148,6 +148,16 @@ let list_mapi f l = aux 0 l ;; +let list_index p = + let rec aux n = + function + [] -> None + | he::_ when p he -> Some (n,he) + | _::tl -> aux (n + 1) tl + in + aux 0 +;; + let rec list_iter_default2 f l1 def l2 = match l1,l2 with | [], _ -> () @@ -239,14 +249,14 @@ let list_concat ?(sep = []) = aux [] let rec list_findopt f l = - let rec aux = function + let rec aux k = function | [] -> None | x::tl -> - (match f x with - | None -> aux tl + (match f x k with + | None -> aux (succ k) tl | Some _ as rc -> rc) in - aux l + aux 0 l let split_nth n l = let rec aux acc n l =