[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