[Agda] tuple pattern sugar

[Nils Anders Danielsson]

On 2013-01-28 19:38, Wolfram Kahl wrote:
> Would it work better to enforce:
>
>     "((just x) : Maybe A) → …"
>
> , that is,
>
>    (APAT : A) -> B
>
> where APAT is ``atomic pattern'' (variable, zero-ary constructor, parenthesised pattern)?

I think so, given that you remove "zero-ary constructor" from your list.

However, I'm not convinced that it is a good idea to make the syntax
more complicated in this way.

-- 
/NAD