[Agda] tuple pattern sugar

[Serge D. Mechveliani]

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