[Agda] tuple pattern sugar

[Darryl]

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.
 
- darryl



________________________________
From: Dmytro Starosud <d.starosud at gmail.com>
To: Serge D. Mechveliani <mechvel at botik.ru> 
Cc: agda at lists.chalmers.se 
Sent: Thursday, January 24, 2013 1:24 PM
Subject: Re: [Agda] tuple pattern sugar


Yes, I am also suffering from it, but not often.

Best regards,
Dmytro 


2013/1/24 Serge D. Mechveliani <mechvel at botik.ru>

On Thu, Jan 24, 2013 at 04:50:59PM +0200, Dmytro Starosud wrote:
>> Ah, sorry, didn't notice that Level3 is tuple :)
>> For this you can use let-bindings:
>>
>> \all {t : Level3} let (x , y , z) = t in (A : Set x) (B : Set y) ...
>>
>
>Yes. I have also discovered the possibility of this `let'.
>Initially, it was not parsed, because I have forgotten to import _,_
>
>(the report is only  "cannot parse",
>and it is difficult to guess and recall of importing _,_).
>
>Thanks,
>
>------
>Sergei
>

_______________________________________________
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/20130124/c8c80e7f/attachment.html