@@ -110,6 +110,20 @@ drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
110110drop Z xs = xs
111111drop (S k) (x :: xs) = drop k xs
112112
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
116+takeUpto Z ys = []
117+takeUpto x [] = rewrite minimumZeroZeroLeft x in []
118+takeUpto (S x) (y::ys) = y :: takeUpto x ys
119+
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
124+dropUpto x [] = []
125+dropUpto (S x) (y :: ys) = dropUpto x ys
126+
113127||| Take the longest prefix of a Vect such that all elements satisfy some
114128||| Boolean predicate.
115129|||