[Agda] When catchall does not help.

Thu Jun 8 21:05:30 CEST 2017

The contruct function uses catchall.

https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLL.agda#L604

Then have a look at the function that proves a property that uses contruct
at its type:

https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLLProp.agda#L1442
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170608/7615b1b1/attachment.html>