vecs.idr

module Main
import Data.Vect

toVec : List a -> (n : Nat ** Vect n a)
toVec [] = (_ ** [])
toVec (x::xs) with (toVec xs)
    | (k ** v) = (S k ** x :: v)

myFun : Vect n1 Int -> Vect n2 Int -> LTE n1 n2 -> Int
myFun xs ys p = foldr (+) 0 xs

toInt : String -> Int
toInt = cast

main : IO ()
main = do
    s1 <- getLine   
    let (n1 ** v1) = toVec $ map toInt $ words s1
    s2 <- getLine   
    let (n2 ** v2) = toVec $ map toInt $ words s2
    case isLTE n1 n2 of
        Yes p => printLn $ myFun v1 v2 p
        No _ => putStrLn "first list was too long"