<div dir="ltr">Aha! Good point. I hadn't noticed that underscore lets me achieve my goal.<div><br></div><div>Unfortunately, using underscore takes up twice as many lines. That's not a big deal for a single expression, but is a problem if I want to, for instance, give a checked signature for every import from a module.</div><div><br></div><div>Cheers, -- P</div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><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></div></div>
<br><div class="gmail_quote">On 6 March 2018 at 17:30, Larrytheliquid <span dir="ltr"><<a href="mailto:larrytheliquid@gmail.com" target="_blank">larrytheliquid@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div>Agda does have underscore definitions, which do not add new identifiers:<br><br><div>\begin{code}</div></div>_ : type_1<br></div>_ = term_1<br>...<br></div>_ : type_n<br></div>_ = term_n<br><div>\end{code}</div><br></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Tue, Mar 6, 2018 at 2:12 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr"><div>A construct like the following would be handy, especially for literate Agda.</div><div>\begin{code}</div><div>check</div><div>  term_1 : type_1</div><div>  ...</div><div>  term_n : type_n</div><div>\end{code}</div><div>Agda checks that each given term has the given type, and typesets the code, but it introduces no new identifiers and has no effect on the other code.<br></div><div><br></div><div>Such a construct can allow one to include examples in the text that are checked by Agda, and hence make the text more reliable. Another use might be to give types for identifiers imported from elsewhere, making the code easier to read and allowing Agda to catch any misunderstandings.</div><div><br></div><div>Is a feature like this available? Would it be hard to add?</div><div><br></div><div>Adding `check` as a keyword would harm backward compatibility, is there another choice that might be better?</div><div><br></div><div>Cheers, -- P</div><div><br clear="all"><div><div class="m_-7555317225670827435m_4347579933891084250gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><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/<wbr>wadler/</a></span></div></div></div></div></div>
</div></div>
<br></div></div>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><span class="HOEnZb"><font color="#888888"><br><br clear="all"><br>-- <br><div class="m_-7555317225670827435gmail_signature" data-smartmail="gmail_signature">Respectfully,<br>Larry Diehl<br></div>
</font></span></div>
</blockquote></div><br></div>