Idris的读写

Question

我正在学习"Idris“的第一步。我正在使用本教程：http://docs.idris-lang.org/en/latest/tutorial/starting.html

我创建了名为"hello.idr“的文件。该文件的内容如下：

module Main

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

我在shell提示符下输入了这一行：“idris hello.idr -o hello”，但是发生了一些无法解释的事情。

​

Answer 1

使用

module Main

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

一切都正常运作。

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

如果没有，我假设您安装的idris已经损坏，根据操作系统的不同，您需要遵循不同的步骤来安装二进制安装。

对于OS，我只是推荐brew install idris或者看一下https://www.idris-lang.org/download/