[Agda] Epic backend question: EpicInclude.e doesn't compile

Hans Peter Würmli hanspeter_wuermli at genevaassociation.org
Tue Dec 2 16:17:09 CET 2014


Trying to compile a simple agda programme with the epic backend ran into
problems. Installing Agda-2.4.2.2 with ghc-7.8.3 and emacs-mode (on
Linux) work flawlessly. Equally, the MAlonzo backend works fine.

Trying out the Epic backend, I ran into problems already with a sample
programme using the stdlib-0.9 when epic compiles EpicInclude.e:

"Compilation error: epic: user error (Unknown name primShowString)"

Trying a simple fix, adding

    primShowString (xs : String) -> String = xs


to EpicInclude.e avoided this error message, but primShowChar became
unknown to the compiler. Trying to fix this with

    primShowChar (c : Int) -> String = charToString c

brought another error I couldn't correct anymore:

"Compilation error:
epic: user error (AgdaPrelude.e:67:Parse error at  (s : String) -> Int =
foreign Int "strl ...)"

which could of course be caused by a wrong definition of primShowChar.


Any help is appreciated.

Hans Peter
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141202/af18ee1c/attachment.html


More information about the Agda mailing list