[Agda] tuple pattern sugar

[Serge D. Mechveliani]

On Thu, Jan 24, 2013 at 03:35:29PM -0800, 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.
>  
> - darryl


I join this suggestion. With this, nice expressions like

  f : ((c , c' , l') : Tuple3) -> Foo c -> Foo' c c' l'

will work.

------
Sergei


> ________________________________
> 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