git.iko.soy/Idris-dev
on master help sign in
Formatting cleanups in Prelude.Vect
e280f8dDavid Raymond Christiansen
libs/prelude/Prelude/Vect.idr+10−10
compare with master
unifiedsplit
@@ -37,7 +37,7 @@ length (x::xs) = 1 + length xs
37
37
38||| Show that the length function on vectors in fact calculates the length
38||| Show that the length function on vectors in fact calculates the length
39private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
39private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n
40−lengthCorrect Z [] = refl
40+lengthCorrect Z [] = refl
41lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl
41lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl
42
42
43--------------------------------------------------------------------------------
43--------------------------------------------------------------------------------
@@ -66,7 +66,7 @@ init (x::y::ys) = x :: init (y::ys)
66index : Fin n -> Vect n a -> a
66index : Fin n -> Vect n a -> a
67index fZ (x::xs) = x
67index fZ (x::xs) = x
68index (fS k) (x::xs) = index k xs
68index (fS k) (x::xs) = index k xs
69−index fZ [] impossible
69+index fZ [] impossible
70
70
71||| Insert an element at a particular index
71||| Insert an element at a particular index
72insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a
72insertAt : 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
79deleteAt fZ (x::xs) = xs
79deleteAt fZ (x::xs) = xs
80deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
80deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs
81deleteAt {n = Z} (fS k) (x::xs) = absurd k
81deleteAt {n = Z} (fS k) (x::xs) = absurd k
82−deleteAt _ [] impossible
82+deleteAt _ [] impossible
83
83
84||| Replace an element at a particlar index with another
84||| Replace an element at a particlar index with another
85replaceAt : Fin n -> t -> Vect n t -> Vect n t
85replaceAt : Fin n -> t -> Vect n t -> Vect n t
@@ -101,13 +101,13 @@ updateAt (fS k) f (x::xs) = x :: updateAt k f xs
101||| Get the first m elements of a Vect
101||| Get the first m elements of a Vect
102||| @ m the number of elements to take
102||| @ m the number of elements to take
103take : (n : Nat) -> Vect (n + m) a -> Vect n a
103take : (n : Nat) -> Vect (n + m) a -> Vect n a
104−take Z xs = []
104+take Z xs = []
105take (S k) (x :: xs) = x :: take k xs
105take (S k) (x :: xs) = x :: take k xs
106
106
107||| Remove the first m elements of a Vect
107||| Remove the first m elements of a Vect
108||| @ m the number of elements to remove
108||| @ m the number of elements to remove
109drop : (n : Nat) -> Vect (n + m) a -> Vect m a
109drop : (n : Nat) -> Vect (n + m) a -> Vect m a
110−drop Z xs = xs
110+drop Z xs = xs
111drop (S k) (x :: xs) = drop k xs
111drop (S k) (x :: xs) = drop k xs
112
112
113--------------------------------------------------------------------------------
113--------------------------------------------------------------------------------
@@ -142,7 +142,7 @@ intersperse sep (x::xs) = x :: intersperse' sep xs
142fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
142fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a
143fromList' ys [] = ys
143fromList' ys [] = ys
144fromList' {n} ys (x::xs) =
144fromList' {n} ys (x::xs) =
145− rewrite (plusSuccRightSucc (length xs) n) ==>
145+ rewrite (plusSuccRightSucc (length xs) n) ==>
146 Vect (plus (length xs) (S n)) a in
146 Vect (plus (length xs) (S n)) a in
147 fromList' (x::ys) xs
147 fromList' (x::ys) xs
148
148
@@ -207,7 +207,7 @@ instance (Eq a) => Eq (Vect n a) where
207--------------------------------------------------------------------------------
207--------------------------------------------------------------------------------
208
208
209instance Ord a => Ord (Vect n a) where
209instance Ord a => Ord (Vect n a) where
210− compare [] [] = EQ
210+ compare [] [] = EQ
211 compare (x::xs) (y::ys) =
211 compare (x::xs) (y::ys) =
212 if x /= y then
212 if x /= y then
213 compare x y
213 compare x y
@@ -455,18 +455,18 @@ catMaybes ((Just j)::xs) with (catMaybes xs)
455 | (_ ** tail) = (_ ** j::tail)
455 | (_ ** tail) = (_ ** j::tail)
456
456
457diag : Vect n (Vect n a) -> Vect n a
457diag : Vect n (Vect n a) -> Vect n a
458−diag [] = []
458+diag [] = []
459diag ((x::xs)::xss) = x :: diag (map tail xss)
459diag ((x::xs)::xss) = x :: diag (map tail xss)
460
460
461range : Vect n (Fin n)
461range : Vect n (Fin n)
462−range {n=Z} = []
462+range {n=Z} = []
463range {n=S _} = fZ :: map fS range
463range {n=S _} = fZ :: map fS range
464
464
465||| Transpose a Vect of Vects, turning rows into columns and vice versa.
465||| Transpose a Vect of Vects, turning rows into columns and vice versa.
466|||
466|||
467||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
467||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
468transpose : Vect m (Vect n a) -> Vect n (Vect m a)
468transpose : Vect m (Vect n a) -> Vect n (Vect m a)
469−transpose [] = replicate _ []
469+transpose [] = replicate _ []
470transpose (x :: xs) = zipWith (::) x (transpose xs)
470transpose (x :: xs) = zipWith (::) x (transpose xs)
471
471
472--------------------------------------------------------------------------------
472--------------------------------------------------------------------------------