[Agda] tuple pattern sugar

[Wolfram Kahl]

On Mon, Jan 28, 2013 at 02:02:05PM +0100, Nils Anders Danielsson wrote:
> On 2013-01-25 00:35, Darryl wrote:
> >this could actually be a good explanation of what the sugar for this stuff 
> >would be.
> >
> >for a pattern PAT
> >
> >(PAT : A) -> B
> >
> >desugars to
> >
> >(x : A) -> let PAT = x in B
> >
> >this shouldn't break anything, and could be added as an option.
> 
> This could break existing code. For instance, "(just x : Maybe A) → …"
> currently introduces /two/ variables.


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)?


Wolfram