[Agda] tuple pattern sugar

Darryl psygnisfive at yahoo.com
Fri Jan 25 00:35:29 CET 2013

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,

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 _,_).

Agda mailing list
Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130124/c8c80e7f/attachment.html

More information about the Agda mailing list