Error compiling Hello World with Agda 2.5.4.2 at command line

1
votes

Given the following Agda program:

module hello-world where

open import Agda.Builtin.IO
open import Agda.Builtin.Unit
open import Agda.Builtin.String

postulate
  putStrLn : String -> ⊤

{-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
{-# COMPILE GHC putStrLn = Text.putStrLn #-}

main : IO ⊤
main = putStrLn "Hello, World!"

I type the following at the command line:

agda --compile hello-world.agda

and get the following output:

Checking hello-world (C:\Projects\2019-06-14-MyAgda\hello-world.agda).
C:\Projects\2019-06-14-MyAgda\hello-world.agda:14,8-32

There is no .exe file in the directory where I run agda from. Please can anyone help?

1
agda

1 Answers

3
votes

I declared putStrLn as follows:

postulate
  putStrLn : String -> ⊤

The correct declaration is, of course

postulate
  putStrLn : String -> IO ⊤