# [Agda] tuple pattern sugar

Serge D. Mechveliani mechvel at botik.ru
Thu Jan 24 15:36:19 CET 2013

(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
`