@@ -100,17 +100,15 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
100100
101101||| Get the first m elements of a Vect
102102||| @ m the number of elements to take
103−take : {n : Nat} -> (m : Fin (S n)) -> Vect n a -> Vect (cast m) a
104−take (fS k) [] = FinZElim k
105−take fZ _ = []
106−take (fS k) (x::xs) = x :: take k xs
103+take : (n : Nat) -> Vect (n + m) a -> Vect n a
104+take Z xs = []
105+take (S k) (x :: xs) = x :: take k xs
107106
108107||| Remove the first m elements of a Vect
109108||| @ m the number of elements to remove
110−drop : (m : Fin (S n)) -> Vect n a -> Vect (n - cast m) a
111−drop (fS k) [] = FinZElim k
112−drop fZ xs ?= xs
113−drop (fS k) (x::xs) = drop k xs
109+drop : (n : Nat) -> Vect (n + m) a -> Vect m a
110+drop Z xs = xs
111+drop (S k) (x :: xs) = drop k xs
114112
115113--------------------------------------------------------------------------------
116114-- Transformations
@@ -407,7 +405,7 @@ nub = nubBy (==)
407405||| It is equivalent to (take n xs, drop n xs)
408406||| @ m the index to split at
409407||| @ xs the Vect to split in two
410−splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)
408+splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
411409splitAt n xs = (take n xs, drop n xs)
412410
413411--------------------------------------------------------------------------------
@@ -489,12 +487,6 @@ vectAppendAssociative (x :: xs) ys zs =
489487-- Proofs
490488--------------------------------------------------------------------------------
491489
492−Prelude.Vect.drop_lemma_1 = proof {
493− intros;
494− rewrite sym (minusZeroRight n);
495− trivial;
496−}
497−
498490Prelude.Vect.reverse'_lemma_1 = proof {
499491 intros;
500492 rewrite prf;