[Agda] tuple pattern sugar

[Dmytro Starosud]

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

Regards,
Dmytro

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

> (a beginner question about `sugar')
>
> Please, how to simplify the following code?
>
>  Solve : {c c' l' : Level} -> {A : Set c} -> {sB : Setoid c' l'} -> Set _
>  Solve {_} {_} {_} {A} {sB} =
>            let B    = Setoid.Carrier sB
>                _~~_ = Setoid._~~_    sB
>            in  (f : A -> B) -> (b : B) -> Dec (\exist (\a -> f a ~~ b))
>
> (for this letter I change respectively the two math symbols).
>
> This is for  Agda-2.3.2 MAlonzo.
>
> Generally, it often occurs that
> a) there are many hidden arguments, and
> b) one is forced to write a call like this:  f {_} {_} {_} {_} a b
>    -- too many place holdes.
>
> So I try
>
>   Level3 : Set _
>   Level3 = Level x Level x Level
>
>   Solve : {(c , c' , l') : Level3} -> {A : Set c} -> {sB : Setoid c' l'} ->
>                                                                       Set _
>   Solve {_} {A} {sB} =  ...
>
> But it is not parsed.
> I have an impression that  case ... of \lambda { (x, y, z) -> ... }
> does work.
> And it is desirable to have working the patterns like
> a)  let  (x , y , z) = f u  in ...,
> b)  (c , c' , l') : Level3
> (and records).
> Could the future Agda language make such patterns valid?
>
> 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/3d912971/attachment.html