@@ -37,7 +37,7 @@ length (x::xs) = 1 + length xs
3737
3838||| Show that the length function on vectors in fact calculates the length
3939private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
40−lengthCorrect Z [] = refl
40+lengthCorrect Z [] = refl
4141lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl
4242
4343--------------------------------------------------------------------------------
@@ -66,7 +66,7 @@ init (x::y::ys) = x :: init (y::ys)
6666index : Fin n -> Vect n a -> a
6767index fZ (x::xs) = x
6868index (fS k) (x::xs) = index k xs
69−index fZ [] impossible
69+index fZ [] impossible
7070
7171||| Insert an element at a particular index
7272insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
@@ -79,7 +79,7 @@ deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a
7979deleteAt fZ (x::xs) = xs
8080deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
8181deleteAt {n = Z} (fS k) (x::xs) = absurd k
82−deleteAt _ [] impossible
82+deleteAt _ [] impossible
8383
8484||| Replace an element at a particlar index with another
8585replaceAt : Fin n -> t -> Vect n t -> Vect n t
@@ -101,13 +101,13 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
101101||| Get the first m elements of a Vect
102102||| @ m the number of elements to take
103103take : (n : Nat) -> Vect (n + m) a -> Vect n a
104−take Z xs = []
104+take Z xs = []
105105take (S k) (x :: xs) = x :: take k xs
106106
107107||| Remove the first m elements of a Vect
108108||| @ m the number of elements to remove
109109drop : (n : Nat) -> Vect (n + m) a -> Vect m a
110−drop Z xs = xs
110+drop Z xs = xs
111111drop (S k) (x :: xs) = drop k xs
112112
113113--------------------------------------------------------------------------------
@@ -142,7 +142,7 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
142142fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
143143fromList' ys [] = ys
144144fromList' {n} ys (x::xs) =
145− rewrite (plusSuccRightSucc (length xs) n) ==>
145+ rewrite (plusSuccRightSucc (length xs) n) ==>
146146 Vect (plus (length xs) (S n)) a in
147147 fromList' (x::ys) xs
148148
@@ -207,7 +207,7 @@ instance (Eq a) => Eq (Vect n a) where
207207--------------------------------------------------------------------------------
208208
209209instance Ord a => Ord (Vect n a) where
210− compare [] [] = EQ
210+ compare [] [] = EQ
211211 compare (x::xs) (y::ys) =
212212 if x /= y then
213213 compare x y
@@ -455,18 +455,18 @@ catMaybes ((Just j)::xs) with (catMaybes xs)
455455 | (_ ** tail) = (_ ** j::tail)
456456
457457diag : Vect n (Vect n a) -> Vect n a
458−diag [] = []
458+diag [] = []
459459diag ((x::xs)::xss) = x :: diag (map tail xss)
460460
461461range : Vect n (Fin n)
462−range {n=Z} = []
462+range {n=Z} = []
463463range {n=S _} = fZ :: map fS range
464464
465465||| Transpose a Vect of Vects, turning rows into columns and vice versa.
466466|||
467467||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
468468transpose : Vect m (Vect n a) -> Vect n (Vect m a)
469−transpose [] = replicate _ []
469+transpose [] = replicate _ []
470470transpose (x :: xs) = zipWith (::) x (transpose xs)
471471
472472--------------------------------------------------------------------------------