[Agda] Bizzare error

[Philip Wadler]

Thank you for the suggestion. Done! (And thank you to James Wood for
pointing out the derelict tabs!) 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 Thu, 30 Sept 2021 at 06:22, Andreas Abel <andreas.abel at ifi.lmu.de> 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.
>
> I definitely see room for better UX, so, welcome to report this on the
> bug tracker.  --Andreas
>
> On 2021-09-27 09:39, Philip Wadler wrote:
> > 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/
> > <http://homepages.inf.ed.ac.uk/wadler/>
> >
> >
> >
> > On Sat, 25 Sept 2021 at 16:27, James Wood <james.wood.100 at strath.ac.uk
> > <mailto: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>
> >      > <http://lambda.lagda.md:522/ <http://lambda.lagda.md:522/>
> >      >
> >      > /Users/wadler/Desktop/Lambda.lagda.md:522
> >     <http://Lambda.lagda.md:522>
> >      > <http://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/>
> >      > <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 <mailto:Agda at lists.chalmers.se>
> >      > https://lists.chalmers.se/mailman/listinfo/agda
> >     <https://lists.chalmers.se/mailman/listinfo/agda>
> >      >
> >
> >     _______________________________________________
> >     Agda mailing list
> >     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> >     https://lists.chalmers.se/mailman/listinfo/agda
> >     <https://lists.chalmers.se/mailman/listinfo/agda>
> >
> >
> > _______________________________________________
> > 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/20211001/9fcc6445/attachment.html>