[Agda] Bizzare error

[Philip Wadler]

Thanks, that fixed it! I did untabify, but appear to have missed one (or
two).

I am still amazed that a tab *in a comment* can cause a lexical error. Is
that a known feature?

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/



On Sat, 25 Sept 2021 at 16:27, James Wood <james.wood.100 at strath.ac.uk>
wrote:

> This email was sent to you by someone outside the University.
> You should only click on links or attachments if you are certain that the
> email is genuine and the content is safe.
>
> Line 561 contains two tab characters. I guess Agda doesn't track
> locations within comment blocks.
>
> Regards,
> James
>
> On 25/09/2021 11:38, Philip Wadler wrote:
> > CAUTION: This email originated outside the University. Check before
> > clicking links or attachments.
> > The attached file yields the following error when compiled via ^C^L:
> >
> > /Users/wadler/Desktop/Lambda.lagda.md:522
> > <http://lambda.lagda.md:522/
> >
> > /Users/wadler/Desktop/Lambda.lagda.md:522
> > <http://lambda.lagda.md:522/
> > 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/
> > <http://homepages.inf.ed.ac.uk/wadler/>
> >
> >
> >
> >
> > The University of Edinburgh is a charitable body, registered in
> > Scotland, with registration number SC005336.
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210927/6fb1a1c1/attachment.html>