<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><div><span>this could actually be a good explanation of what the sugar for this stuff would be.</span></div><div style="background-color: transparent; "><span><br></span></div><div style="background-color: transparent; ">for a pattern PAT</div><div style="background-color: transparent; "><span><br></span></div><div style="background-color: transparent; "><span>(PAT : A) -> B</span></div><div style="background-color: transparent; "><span><br></span></div><div style="background-color: transparent; "><span>desugars to</span></div><div style="background-color: transparent; "><span><br></span></div><div style="background-color: transparent; ">(x : A) -> let PAT = x in B</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial,
helvetica, sans-serif; font-style: normal; ">this shouldn't break anything, and could be added as an option.</div><div></div><div> </div><div>- darryl<br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div class="yui_3_7_2_18_1359061337274_58" style="font-size: 10pt; "><div class="yui_3_7_2_18_1359061337274_61" style="font-family: 'times new roman', 'new york', times, serif; font-size: 12pt; "><div dir="ltr"><font size="2" face="Arial"><hr size="1"><b>From:</b> Dmytro Starosud <d.starosud@gmail.com><br><b>To:</b> Serge D. Mechveliani <mechvel@botik.ru> <br><b>Cc:</b> agda@lists.chalmers.se <br><b>Sent:</b> Thursday, January 24, 2013 1:24 PM<br><b>Subject:</b> Re: [Agda] tuple pattern sugar<br></font></div><br><div id="yiv106680900">Yes, I am also suffering from it, but not
often.<br><br>Best regards,<br>Dmytro <br><br><div class="yiv106680900gmail_quote">2013/1/24 Serge D. Mechveliani <span dir="ltr"><<a rel="nofollow" ymailto="mailto:mechvel@botik.ru" target="_blank" href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>></span><br><blockquote class="yiv106680900gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-color: rgb(204, 204, 204); border-left-style: solid; padding-left: 1ex; "><div class="yiv106680900im">On Thu, Jan 24, 2013 at 04:50:59PM +0200, Dmytro Starosud wrote:<br>> 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><br></div>Yes. I have also discovered the possibility of this `let'.<br>Initially, it was not parsed, because I have forgotten to import _,_<br><br>(the report is only "cannot parse",<br>and it is difficult
to guess and recall of importing _,_).<br><br>Thanks,<br><br>------<br>Sergei<br></blockquote></div><br></div><br>_______________________________________________<br>Agda mailing list<br><a ymailto="mailto:Agda@lists.chalmers.se" 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><br></div></div></div> </div></body></html>