<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="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>
</div></div>