@@ -110,6 +110,20 @@ drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
110drop Z xs = xs
110drop Z xs = xs
111drop (S k) (x :: xs) = drop k xs
111drop (S k) (x :: xs) = drop k xs
113+||| Take up to the first n elements of a Vect if they exist.
114+||| @ n the maximum number of elements to take
115+takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem
117+takeUpto x [] = rewrite minimumZeroZeroLeft x in []
118+takeUpto (S x) (y::ys) = y :: takeUpto x ys
120+||| Drop up to the first n elements of a Vect if they exist.
121+||| @ n the maximum number of elements to remove.
122+dropUpto : (x : Nat) -> Vect n elem -> Vect (n `minus` minimum x n) elem
123+dropUpto Z ys {n} = rewrite minusZeroRight n in ys
125+dropUpto (S x) (y :: ys) = dropUpto x ys
113||| Take the longest prefix of a Vect such that all elements satisfy some
127||| Take the longest prefix of a Vect such that all elements satisfy some
114||| Boolean predicate.
128||| Boolean predicate.