Ah, sorry, didn'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"><<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>