on 7afa310 help sign in
Idris-dev/test/interactive005/interactive005.idr
3 lines 68 B history raw
1||| This is a docstring
2main : IO ()
3main = putStrLn "Hello, World"