[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 
letter as 

(because I hope that this way I send the math symbols as they are).


-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.agda.zip
Type: application/zip
Size: 1324 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20130203/c61bb2c7/Main.agda.zip

More information about the Agda mailing list