2018-03-06 20:12:06 UTC
A construct like the following would be handy, especially for literate Agda.
term_1 : type_1
term_n : type_n
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