@@ -1,6 +1,7 @@
11module Prelude.Vect
22
33import Prelude.Fin
4+import Prelude.Foldable
45import Prelude.Functor
56import Prelude.List
67import Prelude.Nat
@@ -62,13 +63,9 @@ drop (fS k) [] impossible
6263drop (fS k) (x::xs) = drop k xs
6364
6465--------------------------------------------------------------------------------
65−-- Conversions to and from list
66+-- Conversion from list (toList is provided by Foldable)
6667--------------------------------------------------------------------------------
6768
68−toList : Vect n a -> List a
69−toList [] = []
70−toList (x::xs) = x :: toList xs
71−
7269fromList : (l : List a) -> Vect (length l) a
7370fromList [] = []
7471fromList (x::xs) = x :: fromList xs
@@ -123,13 +120,9 @@ instance Functor (Vect n) where
123120-- Folds
124121--------------------------------------------------------------------------------
125122
126−total foldl : (a -> b -> a) -> a -> Vect m b -> a
127−foldl f e [] = e
128−foldl f e (x::xs) = foldl f (f e x) xs
129−
130−total foldr : (a -> b -> b) -> b -> Vect m a -> b
131−foldr f e [] = e
132−foldr f e (x::xs) = f x (foldr f e xs)
123+instance Foldable (Vect n) where
124+ foldr f e [] = e
125+ foldr f e (x::xs) = f x (foldr f e xs)
133126
134127--------------------------------------------------------------------------------
135128-- Special folds
@@ -139,18 +132,6 @@ concat : Vect m (Vect n a) -> Vect (m * n) a
139132concat [] = []
140133concat (v::vs) = v ++ concat vs
141134
142−total and : Vect m Bool -> Bool
143−and = foldr (&&) True
144−
145−total or : Vect m Bool -> Bool
146−or = foldr (||) False
147−
148−total any : (a -> Bool) -> Vect m a -> Bool
149−any p = Vect.or . map p
150−
151−total all : (a -> Bool) -> Vect m a -> Bool
152−all p = Vect.and . map p
153−
154135--------------------------------------------------------------------------------
155136-- Transformations
156137--------------------------------------------------------------------------------