@@ -93,14 +93,14 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
9393-- Subvectors
9494--------------------------------------------------------------------------------
9595
96−||| Get the first m elements of a Vect
97−||| @ m the number of elements to take
96+||| Get the first n elements of a Vect
97+||| @ n the number of elements to take
9898take : (n : Nat) -> Vect (n + m) a -> Vect n a
9999take Z xs = []
100100take (S k) (x :: xs) = x :: take k xs
101101
102−||| Remove the first m elements of a Vect
103−||| @ m the number of elements to remove
102+||| Remove the first n elements of a Vect
103+||| @ n the number of elements to remove
104104drop : (n : Nat) -> Vect (n + m) a -> Vect m a
105105drop Z xs = xs
106106drop (S k) (x :: xs) = drop k xs
@@ -448,7 +448,7 @@ delete = deleteBy (==)
448448||| A tuple where the first element is a Vect of the n first elements and
449449||| the second element is a Vect of the remaining elements of the original Vect
450450||| It is equivalent to (take n xs, drop n xs)
451−||| @ m the index to split at
451+||| @ n the index to split at
452452||| @ xs the Vect to split in two
453453splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
454454splitAt n xs = (take n xs, drop n xs)