[Agda] tuple pattern sugar

[Dmytro Starosud]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130124/a0138441/attachment.html