module agda where
open import IO

main = run (putStrLn "Hello World")