[Agda] FOREIGN GHC pragma triggers parse error
G. Allais
guillaume.allais at ens-lyon.org
Mon Mar 6 16:59:33 CET 2017
Hi,
The master branch of agda-stdlib on github is meant to be used
with the development version of Agda. For released version, you
can get the appropriate tarball on the wiki:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
Best,
On 06/03/17 15:27, Shin-Cheng Mu wrote:
> Hi,
>
> I just installed a fresh copy of Agda using cabal,
> and the latest standard library. When I tried to
> load files with Agda, I get parse errors at
> FOREIGN GHC pragmas. For example, trying Data.Empty:
>
> agda <path to>/src/Data/Empty.agda
>
> <path to>/src/Data/Empty.agda:13,5-5
> <path to>/src/Data/Empty.agda:13,5: Parse error
> FOREIGN<ERROR>
> GHC data AgdaEmpty #-}
> {-# CO...
>
> Why would this happen?
>
> Agda Version 2.5.2
> Standard Library Version 0.13
> GHC Version 8.0.1
>
> and if these matters...
>
> Happy Version 1.19.5
> Alex version 3.2.1
>
> Thank you!
>
> sincerely,
> Shin-Cheng Mu
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170306/84e65c9e/attachment.sig>
More information about the Agda
mailing list