[Agda] tuple pattern sugar

[Nils Anders Danielsson]

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.

-- 
/NAD