[Agda] When catchall does not help.

[Jesper Cockx]

The current best practice is (as far as I know) to use a view type:

```
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

data fun-pattern : A → Set where
  fun-a : fun-pattern a
  fun-other : ∀ {x} → fun-pattern x

fun-view : ∀ x → fun-pattern x
fun-view a = fun-a
fun-view x = fun-other

fun : A → A
fun x with fun-view x
fun .a | fun-a     = b
fun x  | fun-other = j

gun : (x : A) → B (fun x)
gun x with fun-view x
gun .a | fun-a     = q
gun x  | fun-other = w
```

It's still quite a bit of boilerplate, but at least the length doesn't
increase with the number of constructors of A.

-- Jesper


On Tue, Jun 13, 2017 at 1:09 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170613/b5b15e67/attachment-0001.html>