[POPLmark] Type-refinement "challenge"

[Matthieu Sozeau]

Le Vendredi 2 Juin 2006 06:53, Daniel C. Wang a écrit :
> Here is another micro-issue that I think could be improved a bit in all
> systems. I wouldn't call this a hard challenge by any means, but I think
> it's a good way to compare how the various systems can capture this very
> common notational pattern effectively.
>

Here's a solution in Coq, with comments:
http://www.lri.fr/~sozeau/repos/POPLmark/typerefinement/sum_non_zero.pdf
The source is in the same directory.

It took me more time to comment than actually doing it. The second part uses 
my Program vernacular but it may be done in much the same way without it.
-- 
Matthieu Sozeau
http://www.lri.fr/~sozeau