Skip to content

Instantly share code, notes, and snippets.

@adituv
Created October 23, 2016 22:05
Show Gist options
  • Save adituv/09333d17fa87baca23e394829d861d8a to your computer and use it in GitHub Desktop.
Save adituv/09333d17fa87baca23e394829d861d8a to your computer and use it in GitHub Desktop.
Idris attempt?
module Main
import Data.Vect
toVect : List a -> ( n:Nat ** Vect n a )
toVect Nil = ( 0 ** Nil )
toVect (x :: xs) with (toVect xs)
| (n ** ys) = ( S n ** x :: ys )
listFromString : String -> List Int
listFromString = map cast . words
test : IO (n:Nat ** Vect n Int)
test = do
xs <- map listFromString getLine
ys <- map listFromString getLine
let ( nx ** xv ) = toVect xs
let ( ny ** yv ) = toVect ys
pure ( (nx + ny) ** (xv ++ yv) )
main :: IO ()
main = do
v <- test
print v
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment