[Agda] Compiling HelloWorld

[Philippe de Rochambeau]

cabal install ieee754 did the trick.

This is the first time I use cabal.

> Le 15 avr. 2020 à 20:12, Philippe de Rochambeau <phiroc at free.fr> a écrit :
> 
> 
> Hello,
> compiling the following code from the 2.6.1 Agda Documentation causes the below error message.
> 
> module HelloWorld where
> 
> open import Agda.Builtin.IO
> open import Agda.Builtin.Unit
> open import Agda.Builtin.String
> 
> postulate
>   putStrLn : String → IO ⊤
> 
> {-# FOREIGN GHC import qualified Data.Text.IO as Text #-}
> {-# COMPILE GHC putStrLn = Text.putStrLn #-}
> 
> main : IO ⊤
> main = putStrLn "Hello, World!"
> 
> 
> Compilation error:
> 
> MAlonzo/RTE.hs:9:1: error:
>     Could not find module ‘Numeric.IEEE’
>     Use -v (or `:set -v` in ghci) to see a list of the files searched for.
>   |
> 9 | import Numeric.IEEE ( IEEE(identicalIEEE, nan) )
>   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> 
> How do you fix it?
> 
> Many thanks.
> 
> Philippe
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200415/6489b8f2/attachment.html>