[Agda] Checking the types of terms

[Larrytheliquid]

Agda does have underscore definitions, which do not add new identifiers:

\begin{code}
_ : type_1
_ = term_1
...
_ : type_n
_ = term_n
\end{code}


On Tue, Mar 6, 2018 at 2:12 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> 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/
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>


-- 
Respectfully,
Larry Diehl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180306/ea556b36/attachment.html>