[Agda] Checking the types of terms

[Philip Wadler]

A construct like the following would be handy, especially for literate Agda.
\begin{code}
check
  term_1 : type_1
  ...
  term_n : type_n
\end{code}
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.

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.

Is a feature like this available? Would it be hard to add?

Adding `check` as a keyword would harm backward compatibility, is there
another choice that might be better?

Cheers, -- 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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/69831085/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/69831085/attachment.ksh>