Ah, sorry, didn&#39;t notice that Level3 is tuple :)<br>For this you can use let-bindings:<br><br>\all {t : Level3} let (x , y , z) = t in (A : Set x) (B : Set y) ...<br><br>Regards,<br>Dmytro <br><br><div class="gmail_quote">
2013/1/24 Serge D. Mechveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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&#39;)<br>
<br>
Please, how to simplify the following code?<br>
<br>
 Solve : {c c&#39; l&#39; : Level} -&gt; {A : Set c} -&gt; {sB : Setoid c&#39; l&#39;} -&gt; Set _<br>
 Solve {_} {_} {_} {A} {sB} =<br>
           let B    = Setoid.Carrier sB<br>
               _~~_ = Setoid._~~_    sB<br>
           in  (f : A -&gt; B) -&gt; (b : B) -&gt; Dec (\exist (\a -&gt; 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&#39; , l&#39;) : Level3} -&gt; {A : Set c} -&gt; {sB : Setoid c&#39; l&#39;} -&gt;<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) -&gt; ... }<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&#39; , l&#39;) : 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>