reading and writing at Idris

Question

I am in my first steps of learing "Idris". I am using this tutorial: http://docs.idris-lang.org/en/latest/tutorial/starting.html

I created file called "hello.idr". The content of the file is :

module Main

main : IO ()
main = putStrLn "Hello world"

I enterd this line at the shell prompt:"idris hello.idr -o hello" but something unexcpeted occurred

Answer 1

With

module Main

main : IO () 
main = putStrLn "Hello world"

everything works as it should.

~$ idris hello.idr -o hello
~$ ./hello
Hello world

If it does not, you have a broken idris installation I would assume, and depending on your OS you need to follow different steps to install a binary installation.

For OS X I simply recommend brew install idris or have a look at https://www.idris-lang.org/download/