@@ -321,6 +321,7 @@ foldr1 f (x::xs) = foldr f x xs
321321||| Foldl without seeding the accumulator
322322foldl1 : (t -> t -> t) -> Vect (S n) t -> t
323323foldl1 f (x::xs) = foldl f x xs
324+
324325--------------------------------------------------------------------------------
325326-- Scans
326327--------------------------------------------------------------------------------
@@ -455,13 +456,26 @@ delete = deleteBy (==)
455456-- Splitting and breaking lists
456457--------------------------------------------------------------------------------
457458
458−||| A tuple where the first element is a Vect of the n first elements and
459−||| the second element is a Vect of the remaining elements of the original Vect
460−||| It is equivalent to (take n xs, drop n xs)
459+||| A tuple where the first element is a `Vect` of the `n` first elements and
460+||| the second element is a `Vect` of the remaining elements of the original.
461+||| It is equivalent to `(take n xs, drop n xs)`, but is more efficient.
461462||| @ n the index to split at
462463||| @ xs the Vect to split in two
463464splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)
464−splitAt n xs = (take n xs, drop n xs)
465+splitAt Z xs = ([], xs)
466+splitAt (S k) (x::xs) =
467+ let (tk, dr) = splitAt k xs
468+ in (x::tk, dr)
469+
470+splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)
471+splitAtTakeDrop Z xs = Refl
472+splitAtTakeDrop (S k) (x::xs) with (splitAt k xs) proof p
473+ | (tk, dr) =
474+ let rec = sym $ trans p $ splitAtTakeDrop k xs
475+ tkp = cong {f=fst} rec
476+ drp = cong {f=snd} rec
477+ in replace {P = \tk' => (x::tk', dr) = (x::take k xs, drop k xs)} tkp $
478+ replace {P = \dr' => (x::take k xs, dr') = (x::take k xs, drop k xs) } drp Refl
465479
466480partition : (elem -> Bool) -> Vect len elem -> ((p ** Vect p elem), (q ** Vect q elem))
467481partition p [] = ((_ ** []), (_ ** []))