чтение и письмо в Идрисе

Question

Я в своих первых шагах поучения "Идрис". Я использую этот учебник: http://docs.idris -lang.org / ru / latest / tutorial / launch.html

Я создал файл с именем "hello.idr". Содержимое файла:

module Main

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

Я ввел эту строку в командной строке: "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 XIпросто порекомендуйте brew install idris или посмотрите https://www.idris -lang.org / download /