[Agda] Bizzare error

[James Wood]

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
>