[Agda] predicate for sub-type
Serge D. Mechveliani
mechvel at botik.ru
Sun Feb 3 15:01:06 CET 2013
I have a beginner question about using a predicate to define a subset.
One variant does type-check, and a `nicer' one does not.
The program (quite small and simple) and questions are attached to this
(because I hope that this way I send the math symbols as they are).
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 1324 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130203/c61bb2c7/Main.agda.zip
More information about the Agda