[Agda] Bizzare error

Philip Wadler wadler at inf.ed.ac.uk
Sat Sep 25 12:38:51 CEST 2021


The attached file yields the following error when compiled via ^C^L:

/Users/wadler/Desktop/Lambda.lagda.md:522,5-5
/Users/wadler/Desktop/Lambda.lagda.md:522,5: Lexical error (you may want to
replace tabs with spaces):
refl<ERROR>

However, if you delete the large commented portion that follows line 522 it
compiles perfectly well. What is the problem? What is a workaround?

I'm using
Agda version 2.6.1.1-fce01db

Go well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210925/56e73d02/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Lambda.lagda.md
Type: text/markdown
Size: 54253 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210925/56e73d02/attachment.bin>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210925/56e73d02/attachment.ksh>


More information about the Agda mailing list