Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
My first Idris function, maybeVect
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment