@@ -234,11 +234,7 @@ unzip3 ((l,c,r)::xs) with (unzip3 xs)
234234
235235instance (Eq a) => Eq (Vect n a) where
236236 (==) [] [] = True
237− (==) (x::xs) (y::ys) =
238− if x == y then
239− xs == ys
240− else
241− False
237+ (==) (x::xs) (y::ys) = x == y && xs == ys
242238
243239
244240--------------------------------------------------------------------------------
@@ -285,7 +281,7 @@ mapMaybe f (x::xs) =
285281-- Folds
286282--------------------------------------------------------------------------------
287283
288−total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
284+foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc
289285foldrImpl f e go [] = go e
290286foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
291287
@@ -326,9 +322,7 @@ scanl f q (x::xs) = q :: scanl f (f q x) xs
326322||| @ xs the vector to search in
327323elemBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n a) -> Bool
328324elemBy p e [] = False
329−elemBy p e (x::xs) with (p e x)
330− | True = True
331− | False = elemBy p e xs
325+elemBy p e (x::xs) = p e x || elemBy p e xs
332326
333327||| Use the default Boolean equality on elements to search for an item
334328||| @ x what to search for
@@ -341,9 +335,7 @@ elem = elemBy (==)
341335||| @ e the key to look for
342336lookupBy : (p : a -> a -> Bool) -> (e : a) -> (xs : Vect n (a, b)) -> Maybe b
343337lookupBy p e [] = Nothing
344−lookupBy p e ((l, r)::xs) with (p e l)
345− | True = Just r
346− | False = lookupBy p e xs
338+lookupBy p e ((l, r)::xs) = if p e l then Just r else lookupBy p e xs
347339
348340||| Find the assocation of some key using the default Boolean equality test
349341lookup : Eq a => a -> Vect n (a, b) -> Maybe b
@@ -355,9 +347,7 @@ lookup = lookupBy (==)
355347||| @ xs what to search for
356348hasAnyBy : (p : a -> a -> Bool) -> (elems : Vect m a) -> (xs : Vect n a) -> Bool
357349hasAnyBy p elems [] = False
358−hasAnyBy p elems (x::xs) with (elemBy p x elems)
359− | True = True
360− | False = hasAnyBy p elems xs
350+hasAnyBy p elems (x::xs) = elemBy p x elems || hasAnyBy p elems xs
361351
362352||| Check if any element of xs is found in elems using the default Boolean equality test
363353hasAny : Eq a => Vect m a -> Vect n a -> Bool
@@ -371,19 +361,15 @@ hasAny = hasAnyBy (==)
371361||| @ p the test to satisfy
372362find : (p : a -> Bool) -> (xs : Vect n a) -> Maybe a
373363find p [] = Nothing
374−find p (x::xs) with (p x)
375− | True = Just x
376− | False = find p xs
364+find p (x::xs) = if p x then Just x else find p xs
377365
378366||| Find the index of the first element of the vector that satisfies some test
379367findIndex : (a -> Bool) -> Vect n a -> Maybe (Fin n)
380368findIndex p [] = Nothing
381−findIndex p (x :: xs) with (p x)
382− | True = Just 0
383− | False = map FS (findIndex p xs)
369+findIndex p (x :: xs) = if p x then Just 0 else map FS (findIndex p xs)
384370
385371||| Find the indices of all elements that satisfy some test
386−total findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
372+findIndices : (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
387373findIndices = findIndices' 0
388374 where
389375 total findIndices' : Nat -> (a -> Bool) -> Vect m a -> (p ** Vect p Nat)
@@ -401,10 +387,10 @@ elemIndexBy p e = findIndex $ p e
401387elemIndex : Eq a => a -> Vect m a -> Maybe (Fin m)
402388elemIndex = elemIndexBy (==)
403389
404−total elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
390+elemIndicesBy : (a -> a -> Bool) -> a -> Vect m a -> (p ** Vect p Nat)
405391elemIndicesBy p e = findIndices $ p e
406392
407−total elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
393+elemIndices : Eq a => a -> Vect m a -> (p ** Vect p Nat)
408394elemIndices = elemIndicesBy (==)
409395
410396--------------------------------------------------------------------------------
@@ -412,14 +398,14 @@ elemIndices = elemIndicesBy (==)
412398--------------------------------------------------------------------------------
413399
414400||| Find all elements of a vector that satisfy some test
415−total filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
416−filter p [] = ( _ ** [] )
417−filter p (x::xs) with (filter p xs)
418− | (_ ** tail) =
419− if p x then
420− (_ ** x::tail)
421− else
422− (_ ** tail)
401+filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
402+filter p [] = ( _ ** [] )
403+filter p (x::xs) =
404+ let (_ ** tail) = filter p xs
405+ in if p x then
406+ (_ ** x::tail)
407+ else
408+ (_ ** tail)
423409
424410||| Make the elements of some vector unique by some test
425411nubBy : (a -> a -> Bool) -> Vect n a -> (p ** Vect p a)
@@ -473,9 +459,7 @@ partition p (x::xs) =
473459isPrefixOfBy : (a -> a -> Bool) -> Vect m a -> Vect n a -> Bool
474460isPrefixOfBy p [] right = True
475461isPrefixOfBy p left [] = False
476−isPrefixOfBy p (x::xs) (y::ys) with (p x y)
477− | True = isPrefixOfBy p xs ys
478− | False = False
462+isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys
479463
480464isPrefixOf : Eq a => Vect m a -> Vect n a -> Bool
481465isPrefixOf = isPrefixOfBy (==)
@@ -490,11 +474,11 @@ isSuffixOf = isSuffixOfBy (==)
490474-- Conversions
491475--------------------------------------------------------------------------------
492476
493−total maybeToVect : Maybe a -> (p ** Vect p a)
477+maybeToVect : Maybe a -> (p ** Vect p a)
494478maybeToVect Nothing = (_ ** [])
495479maybeToVect (Just j) = (_ ** [j])
496480
497−total vectToMaybe : Vect n a -> Maybe a
481+vectToMaybe : Vect n a -> Maybe a
498482vectToMaybe [] = Nothing
499483vectToMaybe (x::xs) = Just x
500484
@@ -505,21 +489,22 @@ vectToMaybe (x::xs) = Just x
505489catMaybes : Vect n (Maybe a) -> (p ** Vect p a)
506490catMaybes [] = (_ ** [])
507491catMaybes (Nothing::xs) = catMaybes xs
508−catMaybes ((Just j)::xs) with (catMaybes xs)
509− | (_ ** tail) = (_ ** j::tail)
492+catMaybes ((Just j)::xs) =
493+ let (_ ** tail) = catMaybes xs
494+ in (_ ** j::tail)
510495
511496diag : Vect n (Vect n a) -> Vect n a
512497diag [] = []
513498diag ((x::xs)::xss) = x :: diag (map tail xss)
514499
515−range : Vect n (Fin n)
500+range : {n : Nat} -> Vect n (Fin n)
516501range {n=Z} = []
517502range {n=S _} = FZ :: map FS range
518503
519504||| Transpose a Vect of Vects, turning rows into columns and vice versa.
520505|||
521506||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`.
522−transpose : Vect m (Vect n a) -> Vect n (Vect m a)
507+transpose : {n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a)
523508transpose [] = replicate _ []
524509transpose (x :: xs) = zipWith (::) x (transpose xs)
525510
@@ -569,11 +554,9 @@ vectAppendAssociative (x :: xs) ys zs =
569554-- DecEq
570555--------------------------------------------------------------------------------
571556
572−total
573557vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
574558vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
575559
576−total
577560vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
578561vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
579562