Skip to content

Instantly share code, notes, and snippets.

@jroesch
Created October 14, 2014 21:14
Show Gist options
  • Save jroesch/3176f3631aab87f63db4 to your computer and use it in GitHub Desktop.
Save jroesch/3176f3631aab87f63db4 to your computer and use it in GitHub Desktop.
dynamic to static idris
module Main
listToVect : (n: Nat) -> List a -> Maybe (Vect n a)
listToVect Z Nil = Just Nil
listToVect n Nil = Nothing
listToVect (S n) (x :: xs) = map (x ::) (listToVect n xs)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment