[Agda] Bizzare error

[Andreas Abel]

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
>