[Agda] tuple pattern sugar
Nils Anders Danielsson
nad at chalmers.se
Mon Jan 28 14:02:05 CET 2013
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.
More information about the Agda