@@ -104,12 +104,36 @@ take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
104104take Z xs = []
105105take (S k) (x :: xs) = x :: take k xs
106106
107+takeTake : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> take n (take (n + m) xs) = take n {m = m + l} (rewrite plusAssociative n m l in xs)
108+takeTake Z m xs = Refl
109+takeTake {l} (S k) m (x :: xs) = rewrite aux (plusAssociative k m l) x xs in cong { f = (x ::) } $ takeTake k m xs
110+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
111+ (x : a) -> (xs : Vect m a) ->
112+ rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
113+ aux Refl x xs = Refl
114+
107115||| Remove the first n elements of a Vect
108116||| @ n the number of elements to remove
109117drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem
110118drop Z xs = xs
111119drop (S k) (x :: xs) = drop k xs
112120
121+dropDrop : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> drop n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop (m + n) xs
122+dropDrop n Z xs = Refl
123+dropDrop {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in dropDrop n k xs
124+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
125+ (x : a) -> (xs : Vect m a) ->
126+ rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
127+ aux Refl x xs = Refl
128+
129+takeDropDropTake : (n : Nat) -> (m : Nat) -> (xs : Vect (m + n + l) a) -> take n (drop m {m = n + l} (rewrite plusAssociative m n l in xs)) = drop m (take (m + n) xs)
130+takeDropDropTake n Z xs = Refl
131+takeDropDropTake {l} n (S k) (x :: xs) = rewrite aux (plusAssociative k n l) x xs in takeDropDropTake n k xs
132+ where aux : {n : Nat} -> {m : Nat} -> (prf : n = m) ->
133+ (x : a) -> (xs : Vect m a) ->
134+ rewrite__impl (\rep => Vect rep a) (rewrite__impl (\rep => S rep = S m) prf Refl) (x :: xs) = x :: rewrite__impl (\rep => Vect rep a) prf xs
135+ aux Refl x xs = Refl
136+
113137||| Take the longest prefix of a Vect such that all elements satisfy some
114138||| Boolean predicate.
115139|||
@@ -188,6 +212,18 @@ fromList l =
188212(++) [] ys = ys
189213(++) (x::xs) ys = x :: xs ++ ys
190214
215+takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns
216+takePrefix [] _ = Refl
217+takePrefix (n :: ns) ms = cong $ takePrefix ns ms
218+
219+dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms
220+dropPrefix [] ms = Refl
221+dropPrefix (_ :: ns) ms = dropPrefix ns ms
222+
223+takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs
224+takeDropConcat Z xs = Refl
225+takeDropConcat (S k) (x :: xs) = cong $ takeDropConcat k xs
226+
191227||| Repeate some value some number of times.
192228|||
193229||| @ len the number of times to repeat it
@@ -567,6 +603,13 @@ implementation Traversable (Vect n) where
567603implementation Show elem => Show (Vect len elem) where
568604 show = show . toList
569605
606+--------------------------------------------------------------------------------
607+-- Uninhabited
608+--------------------------------------------------------------------------------
609+
610+Uninhabited a => Uninhabited (Vect (S n) a) where
611+ uninhabited (x :: _) = uninhabited x
612+
570613--------------------------------------------------------------------------------
571614-- Properties
572615--------------------------------------------------------------------------------
@@ -574,6 +617,9 @@ implementation Show elem => Show (Vect len elem) where
574617vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
575618vectConsCong x xs xs Refl = Refl
576619
620+vectMustBeNil : (xs : Vect Z a) -> xs = []
621+vectMustBeNil [] = Refl
622+
577623vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
578624vectNilRightNeutral [] = Refl
579625vectNilRightNeutral (x :: xs) =