<div dir="ltr">The attached file yields the following error when compiled via ^C^L:<div><br></div><div>/Users/wadler/Desktop/<a href="http://Lambda.lagda.md:522">Lambda.lagda.md:522</a>,5-5<div><div>/Users/wadler/Desktop/<a href="http://Lambda.lagda.md:522">Lambda.lagda.md:522</a>,5: Lexical error (you may want to replace tabs with spaces):<br>refl<ERROR><br><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"><br></div><div>However, if you delete the large commented portion that follows line 522 it compiles perfectly well. What is the problem? What is a workaround?</div><div><br></div><div>I'm using</div><div>Agda version 2.6.1.1-fce01db<br></div><div><br></div><div>Go well, -- P</div><div dir="ltr"><br></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 dir="ltr"><br></div><div dir="ltr"><br></div></div></div></div></div></div></div></div></div></div></div>