I think it is a bad idea to allow such a syntax.<br>Nevertheless, if you don't want to write {_} many times, you can name variable you need:<br><br>f : \all {x} {y} {z} -> Set<br>f {z = z} = _ -- I don't need x and y but only z,<br>
<br>Regards,<br>Dmytro <br><br><div class="gmail_quote">2013/1/24 Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
(a beginner question about `sugar')<br>
<br>
Please, how to simplify the following code?<br>
<br>
Solve : {c c' l' : Level} -> {A : Set c} -> {sB : Setoid c' l'} -> Set _<br>
Solve {_} {_} {_} {A} {sB} =<br>
let B = Setoid.Carrier sB<br>
_~~_ = Setoid._~~_ sB<br>
in (f : A -> B) -> (b : B) -> Dec (\exist (\a -> f a ~~ b))<br>
<br>
(for this letter I change respectively the two math symbols).<br>
<br>
This is for Agda-2.3.2 MAlonzo.<br>
<br>
Generally, it often occurs that<br>
a) there are many hidden arguments, and<br>
b) one is forced to write a call like this: f {_} {_} {_} {_} a b<br>
-- too many place holdes.<br>
<br>
So I try<br>
<br>
Level3 : Set _<br>
Level3 = Level x Level x Level<br>
<br>
Solve : {(c , c' , l') : Level3} -> {A : Set c} -> {sB : Setoid c' l'} -><br>
Set _<br>
Solve {_} {A} {sB} = ...<br>
<br>
But it is not parsed.<br>
I have an impression that case ... of \lambda { (x, y, z) -> ... }<br>
does work.<br>
And it is desirable to have working the patterns like<br>
a) let (x , y , z) = f u in ...,<br>
b) (c , c' , l') : Level3<br>
(and records).<br>
Could the future Agda language make such patterns valid?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br>