My first Idris function, maybeVect

MaybeVect.idr

module MaybeVect

import Data.Vect

maybeVect : (n: Nat) -> List a -> Maybe (Vect n a)
maybeVect Z []        = Just []
maybeVect n []        = Nothing
maybeVect Z xs        = Nothing
maybeVect n (x :: xs) = let S(k) = n in
                            map (\ xs' => x :: xs') (maybeVect k xs)

maybePrepend : a -> Maybe (Vect n a) -> Maybe (Vect (S n) a)
maybePrepend x Nothing = Nothing
maybePrepend x (Just xs) = Just (x :: xs)

maybeVect2 : (n: Nat) -> List a -> Maybe (Vect n a)
maybeVect2 Z []        = Just []
maybeVect2 n []        = Nothing
maybeVect2 Z xs        = Nothing
maybeVect2 n (x :: xs) = let S(k) = n in
                             maybePrepend x (maybeVect2 k xs)
-- maybeVect2 ( n = S(k) ) (x :: xs) =  maybePrepend x (maybeVect2 xs k)
-- maybeVect2 S(k) (x :: xs) = maybePrepend x (maybeVect2 xs k)