[Agda] When catchall does not help.

[Nils Anders Danielsson]

On 2017-06-08 21:05, Apostolis Xekoukoulotakis wrote:
> 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

As far as I understand the CATCHALL pragma can be used if you have
enabled --exact-split, but want to disable this option for a specific
clause. When CATCHALL is used some equations may not hold
definitionally.

-- 
/NAD