Idris attempt?

main.idr

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