Created
October 9, 2019 11:37
-
-
Save thedeemon/b066db73ff9d8ab5df0c63b2e10a6cc4 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment