@@ -93,14 +93,14 @@ updateAt (FS k) f (x::xs) = x :: updateAt k f xs
93-- Subvectors
93-- Subvectors
94--------------------------------------------------------------------------------
94--------------------------------------------------------------------------------
96−||| Get the first m elements of a Vect
96+||| Get the first n elements of a Vect
97−||| @ m the number of elements to take
97+||| @ n the number of elements to take
98take : (n : Nat) -> Vect (n + m) a -> Vect n a
98take : (n : Nat) -> Vect (n + m) a -> Vect n a
99take Z xs = []
99take Z xs = []
100take (S k) (x :: xs) = x :: take k xs
100take (S k) (x :: xs) = x :: take k xs
102−||| Remove the first m elements of a Vect
102+||| Remove the first n elements of a Vect
103−||| @ m the number of elements to remove
103+||| @ n the number of elements to remove
104drop : (n : Nat) -> Vect (n + m) a -> Vect m a
104drop : (n : Nat) -> Vect (n + m) a -> Vect m a
105drop Z xs = xs
105drop Z xs = xs
106drop (S k) (x :: xs) = drop k xs
106drop (S k) (x :: xs) = drop k xs
@@ -448,7 +448,7 @@ delete = deleteBy (==)
448||| A tuple where the first element is a Vect of the n first elements and
448||| A tuple where the first element is a Vect of the n first elements and
449||| the second element is a Vect of the remaining elements of the original Vect
449||| the second element is a Vect of the remaining elements of the original Vect
450||| It is equivalent to (take n xs, drop n xs)
450||| It is equivalent to (take n xs, drop n xs)
451−||| @ m the index to split at
451+||| @ n the index to split at
452||| @ xs the Vect to split in two
452||| @ xs the Vect to split in two
453splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
453splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)
454splitAt n xs = (take n xs, drop n xs)
454splitAt n xs = (take n xs, drop n xs)