<div dir="ltr">Thank you for the suggestion. Done! (And thank you to James Wood for pointing out the derelict tabs!) 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><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 30 Sept 2021 at 06:22, Andreas Abel <<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</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>
I definitely see room for better UX, so, welcome to report this on the<br>
bug tracker. --Andreas<br>
<br>
On 2021-09-27 09:39, Philip Wadler wrote:<br>
> Thanks, that fixed it! I did untabify, but appear to have missed one (or<br>
> two).<br>
><br>
> I am still amazed that a tab *in a comment* can cause a lexical error.<br>
> Is that a known feature?<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>
> On Sat, 25 Sept 2021 at 16:27, James Wood <<a href="mailto:james.wood.100@strath.ac.uk" target="_blank">james.wood.100@strath.ac.uk</a><br>
> <mailto:<a href="mailto:james.wood.100@strath.ac.uk" target="_blank">james.wood.100@strath.ac.uk</a>>> wrote:<br>
><br>
> This email was sent to you by someone outside the University.<br>
> You should only click on links or attachments if you are certain<br>
> 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>
> > <<a href="http://lambda.lagda.md:522/" rel="noreferrer" target="_blank">http://lambda.lagda.md:522/</a> <<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>
> > <<a href="http://lambda.lagda.md:522/" rel="noreferrer" target="_blank">http://lambda.lagda.md:522/</a> <<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<br>
> line 522<br>
> > it compiles perfectly well. What is the problem? What is a<br>
> 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>
> > <<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> <mailto:<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>
> <<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> <mailto:<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>
> <<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>
><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>