@@ -51,15 +51,14 @@ replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs
5151-- Subvectors
5252--------------------------------------------------------------------------------
5353
54−take : Fin n -> Vect n a -> (p ** Vect p a)
55−take fZ xs = (_ ** [])
56−take (fS k) [] impossible
57−take (fS k) (x::xs) with (take k xs)
58− | (_ ** tail) = (_ ** x::tail)
59−
60−drop : Fin n -> Vect n a -> (p ** Vect p a)
61−drop fZ xs = (_ ** xs)
62−drop (fS k) [] impossible
54+take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
55+take (fS k) [] = FinZElim k
56+take fZ _ = []
57+take (fS k) (x::xs) = x :: take k xs
58+
59+drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
60+drop (fS k) [] = FinZElim k
61+drop fZ xs ?= xs
6362drop (fS k) (x::xs) = drop k xs
6463
6564--------------------------------------------------------------------------------
@@ -311,6 +310,12 @@ range {n=S _} = fZ :: map fS range
311310-- Proofs
312311--------------------------------------------------------------------------------
313312
313+Prelude.Vect.drop_lemma_1 = proof {
314+ intros;
315+ rewrite sym (minusZeroRight n);
316+ trivial;
317+}
318+
314319Prelude.Vect.reverse'_lemma_2 = proof {
315320 intros;
316321 rewrite (plusSuccRightSucc m n1);