[Agda] tuple pattern sugar
Dmytro Starosud
d.starosud at gmail.com
Thu Jan 24 15:45:55 CET 2013
I think it is a bad idea to allow such a syntax.
Nevertheless, if you don't want to write {_} many times, you can name
variable you need:
f : \all {x} {y} {z} -> Set
f {z = z} = _ -- I don't need x and y but only z,
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/6a047ece/attachment.html
More information about the Agda
mailing list