<div dir="ltr"><div>True, the problem is that in some cases, you would like it to hold definitionally.<br><br></div>The below example is one such case. gun has the same behavior for all A except a.<br><div><div><div><br>```<br><div>module test where<br><br>data A : Set where<br>  a b c d e f g h i j : A<br><br>data B : A → Set where<br>  q : ∀ {x} → B x<br>  w : B j<br><br><br>fun : A → A<br>fun a = b<br>fun x = j<br><br><br>--gun : (x : A) → B (fun x)<br>--gun a = q<br>--{-# SOMETHING -#}<br>--gun x = w<br>--<br><br>gun : (x : A) → B (fun x)<br>gun a = q<br>gun b = w<br>gun c = w<br>gun d = w<br>gun e = w<br>gun f = w<br>gun g = w<br>gun h = w<br>gun i = w<br>gun j = w<br><br>```<br></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 13, 2017 at 12:47 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On 2017-06-08 21:05, Apostolis Xekoukoulotakis wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The contruct function uses catchall.<br>
<br>
<a href="https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLL.agda#L604" rel="noreferrer" target="_blank">https://github.com/xekoukou/sp<wbr>arrow/blob/d00493afcafc1fb0d2e<wbr>e08781de09fd246523629/agda/<wbr>SetLL.agda#L604</a><br>
<br>
Then have a look at the function that proves a property that uses contruct at its type:<br>
<br>
<a href="https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2ee08781de09fd246523629/agda/SetLLProp.agda#L1442" rel="noreferrer" target="_blank">https://github.com/xekoukou/sp<wbr>arrow/blob/d00493afcafc1fb0d2e<wbr>e08781de09fd246523629/agda/<wbr>SetLLProp.agda#L1442</a><br>
</blockquote>
<br></div></div>
As far as I understand the CATCHALL pragma can be used if you have<br>
enabled --exact-split, but want to disable this option for a specific<br>
clause. When CATCHALL is used some equations may not hold<br>
definitionally.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>