@@ -36,6 +36,21 @@ index (fS k) (x::xs) = index k xs
3636index fO [] impossible
3737index (fS _) [] impossible
3838
39+--------------------------------------------------------------------------------
40+-- Subvectors
41+--------------------------------------------------------------------------------
42+
43+take : Fin n -> Vect a n -> (p ** Vect a p)
44+take fO xs = (_ ** [])
45+take (fS k) [] impossible
46+take (fS k) (x::xs) with (take k xs)
47+ | (_ ** tail) = (_ ** x::tail)
48+
49+drop : Fin n -> Vect a n -> (p ** Vect a p)
50+drop fO xs = (_ ** xs)
51+drop (fS k) [] impossible
52+drop (fS k) (x::xs) = drop k xs
53+
3954--------------------------------------------------------------------------------
4055-- Conversions to and from list
4156--------------------------------------------------------------------------------
@@ -64,6 +79,16 @@ total map : (a -> b) -> Vect a n -> Vect b n
6479map f [] = []
6580map f (x::xs) = f x :: map f xs
6681
82+-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
83+--mapMaybe : (a -> Maybe b) -> Vect a n -> (p ** Vect b p)
84+--mapMaybe f [] = (_ ** [])
85+--mapMaybe f (x::xs) = mapMaybe' (f x)
86+-- XXX: working around the type restrictions on case statements
87+-- where
88+-- mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)
89+-- mapMaybe' Nothing (n ** tail) = (n ** tail)
90+-- mapMaybe' (Just j) (n ** tail) = (S n ** j::tail)
91+
6792--------------------------------------------------------------------------------
6893-- Folds
6994--------------------------------------------------------------------------------
@@ -217,8 +242,6 @@ nub = nubBy (==)
217242-- Splitting and breaking lists
218243--------------------------------------------------------------------------------
219244
220−-- XXX: todo
221−
222245--------------------------------------------------------------------------------
223246-- Predicates
224247--------------------------------------------------------------------------------