@@ -104,9 +104,9 @@ unzip ((l, r)::xs) with (unzip xs)
104104-- Maps
105105--------------------------------------------------------------------------------
106106
107−map : (a -> b) -> Vect n a -> Vect n b
108−map f [] = []
109−map f (x::xs) = f x :: map f xs
107+instance Functor (Vect n) where
108+ map f [] = []
109+ map f (x::xs) = f x :: map f xs
110110
111111-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
112112--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)
@@ -145,10 +145,10 @@ total or : Vect m Bool -> Bool
145145or = foldr (||) False
146146
147147total any : (a -> Bool) -> Vect m a -> Bool
148−any p = Vect.or . Vect.map p
148+any p = Vect.or . map p
149149
150150total all : (a -> Bool) -> Vect m a -> Bool
151−all p = Vect.and . Vect.map p
151+all p = Vect.and . map p
152152
153153--------------------------------------------------------------------------------
154154-- Transformations
@@ -317,6 +317,10 @@ catMaybes (Nothing::xs) = catMaybes xs
317317catMaybes ((Just j)::xs) with (catMaybes xs)
318318 | (_ ** tail) = (_ ** j::tail)
319319
320+diag : Vect n (Vect n a) -> Vect n a
321+diag [] = []
322+diag ((x::xs)::xss) = x :: diag (map tail xss)
323+
320324range : Vect n (Fin n)
321325range =
322326 reverse range_