[Agda] When catchall does not help.

[Apostolis Xekoukoulotakis]

True, the problem is that in some cases, you would like it to hold
definitionally.

The below example is one such case. gun has the same behavior for all A
except a.

```
module test where

data A : Set where
  a b c d e f g h i j : A

data B : A → Set where
  q : ∀ {x} → B x
  w : B j


fun : A → A
fun a = b
fun x = j


--gun : (x : A) → B (fun x)
--gun a = q
--{-# SOMETHING -#}
--gun x = w
--

gun : (x : A) → B (fun x)
gun a = q
gun b = w
gun c = w
gun d = w
gun e = w
gun f = w
gun g = w
gun h = w
gun i = w
gun j = w

```

On Tue, Jun 13, 2017 at 12:47 PM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 2017-06-08 21:05, Apostolis Xekoukoulotakis wrote:
>
>> The contruct function uses catchall.
>>
>> https://github.com/xekoukou/sparrow/blob/d00493afcafc1fb0d2e
>> e08781de09fd246523629/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/d00493afcafc1fb0d2e
>> e08781de09fd246523629/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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170613/a2737136/attachment.html>