<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">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><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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_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>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">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature" data-smartmail="gmail_signature">Respectfully,<br>Larry Diehl<br></div>
</div>