<div dir="ltr"><div><div>The current best practice is (as far as I know) to use a view type:<br><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>data fun-pattern : A → Set where<br>  fun-a : fun-pattern a<br>  fun-other : ∀ {x} → fun-pattern x<br><br>fun-view : ∀ x → fun-pattern x<br>fun-view a = fun-a<br>fun-view x = fun-other<br><br>fun : A → A<br>fun x with fun-view x<br>fun .a | fun-a     = b<br>fun x  | fun-other = j<br><br>gun : (x : A) → B (fun x)<br>gun x with fun-view x<br>gun .a | fun-a     = q<br>gun x  | fun-other = w<br>```<br><br></div>It's still quite a bit of boilerplate, but at least the length doesn't increase with the number of constructors of A.<br><br></div>-- Jesper<br><div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 13, 2017 at 1:09 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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="HOEnZb"><div class="h5"><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="m_5266777878846962986HOEnZb"><div class="m_5266777878846962986h5">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/Set<wbr>LL.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/Set<wbr>LLProp.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="m_5266777878846962986HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div>
</div></div><br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>