From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 24 Sep 2008 14:48:36 +0000 (+0000)
Subject: added skip function
X-Git-Tag: make_still_working~4747
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=abc5b4352a4ad787ede7122e2239ee44132886dd;p=helm.git

added skip function
---

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index fe0f417cd..6af86f9cd 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -529,3 +529,10 @@ let list_seq start stop =
     aux start
 ;;
 
+let rec list_skip n l =
+  match n,l with
+  | 0,_ -> l
+  | n,_::l -> list_skip (n-1) l
+  | _, [] -> assert false
+;;
+
diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index 96e7a398c..a92389fea 100644
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -108,6 +108,9 @@ val list_forall_default3: ('a -> 'b -> 'c -> bool) -> 'a list -> 'b list -> 'c -
    * @raise Failure when List.length l < n *)
 val split_nth: int -> 'a list -> 'a list * 'a list
 
+ (** skip [n] [l] skips the first n elements of l *)
+val list_skip : int -> 'a list -> 'a list
+
 val mk_list: 'a -> int -> 'a list
 
 (* makes the list [start; ...; stop - 1] *)