<div dir="ltr">Thanks, that fixed it! I did untabify, but appear to have missed one (or two).<div><br></div><div>I am still amazed that a tab *in a comment* can cause a lexical error. Is that a known feature?</div><div><br></div><div>Go well, -- P<div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 25 Sept 2021 at 16:27, James Wood <<a href="mailto:james.wood.100@strath.ac.uk">james.wood.100@strath.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">This email was sent to you by someone outside the University.<br>
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.<br>
<br>
Line 561 contains two tab characters. I guess Agda doesn't track<br>
locations within comment blocks.<br>
<br>
Regards,<br>
James<br>
<br>
On 25/09/2021 11:38, Philip Wadler wrote:<br>
> CAUTION: This email originated outside the University. Check before<br>
> clicking links or attachments.<br>
> The attached file yields the following error when compiled via ^C^L:<br>
><br>
> /Users/wadler/Desktop/<a href="http://Lambda.lagda.md:522" rel="noreferrer" target="_blank">Lambda.lagda.md:522</a><br>
> <<a href="http://lambda.lagda.md:522/" rel="noreferrer" target="_blank">http://lambda.lagda.md:522/</a><br>
><br>
> /Users/wadler/Desktop/<a href="http://Lambda.lagda.md:522" rel="noreferrer" target="_blank">Lambda.lagda.md:522</a><br>
> <<a href="http://lambda.lagda.md:522/" rel="noreferrer" target="_blank">http://lambda.lagda.md:522/</a><br>
> Lexical error (you may want to replace tabs with spaces):<br>
> refl<ERROR><br>
><br>
> However, if you delete the large commented portion that follows line 522<br>
> it compiles perfectly well. What is the problem? What is a workaround?<br>
><br>
> I'm using<br>
> Agda version 2.6.1.1-fce01db<br>
><br>
> Go well, -- P<br>
><br>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,<br>
> .   /\ School of Informatics, University of Edinburgh<br>
> .  /  \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a><br>
> <<a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a>><br>
><br>
><br>
><br>
><br>
> The University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>