idris-0.9.15: test/interactive005/interactive005.idr

||| This is a docstring
main : IO ()
main = putStrLn "Hello, World"