[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