<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Yeah, it works fine for me.</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>$ agda --version</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color:
transparent; font-style: normal; "><span>Agda version 2.3.2<br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span>Full code that I used was</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0,
0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><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; "><br></div><div style="background-color: transparent; color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; font-style: normal; ">open import Data.Unit</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">module Experiment where</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">data P : ⊤ → Set where</div><div style="background-color: transparent; "> pt : P tt</div><div style="background-color: transparent; "><br></div><div style="background-color: transparent; ">test : (t : ⊤) → P
t</div><div style="background-color: transparent; ">test t with t</div><div style="background-color: transparent; ">test t | tt = result</div><div style="background-color: transparent; "> where postulate result : P t</div><div style="background-color: transparent; "><br></div></span></div><div></div><div> </div><div><br></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 style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div> <div style="font-family: arial, helvetica, sans-serif; font-size: 10pt; "> <div 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><span style="font-weight:bold;">From:</span></b> Andreas Abel
<andreas.abel@ifi.lmu.de><br> <b><span style="font-weight: bold;">To:</span></b> Darryl McAdams <psygnisfive@yahoo.com> <br><b><span style="font-weight: bold;">Cc:</span></b> Agda List <agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Wednesday, March 6, 2013 1:56 PM<br> <b><span style="font-weight: bold;">Subject:</span></b> Re: [Agda] with match changes the result type of a function<br> </font> </div> <br>
If I give "result", then I get<br><br> t != tt of type ⊤<br> when checking that the expression result has type P tt<br><br>Are you sure it works for you? If yes which system do you have?<br><br>Cheers,<br>Andreas<br><br>On 06.03.13 4:43 AM, Darryl McAdams wrote:<br>> For what it's worth, the problematic code as quoted here type checks for<br>> me. That is to say, this statement:<br>><br>> "Note that result is not accepted"<br>><br>> is false on my system.<br>> - darryl<br>> ------------------------------------------------------------------------<br>> *From:* Dominique Devriese <<a ymailto="mailto:dominique.devriese@cs.kuleuven.be" href="mailto:dominique.devriese@cs.kuleuven.be">dominique.devriese@cs.kuleuven.be</a>><br>> *To:* Serge D. Mechveliani <<a ymailto="mailto:mechvel@botik.ru" href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>> *Cc:* Agda List <<a
ymailto="mailto:agda@lists.chalmers.se" href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>> *Sent:* Tuesday, March 5, 2013 11:05 AM<br>> *Subject:* Re: [Agda] with match changes the result type of a function<br>><br>> Serge,<br>><br>> I've taken a brief look at your code, and I think this is a simplified<br>> version of your problem:<br>><br>> module test where<br>><br>> data ⊤ : Set where tt : ⊤<br>><br>> data P : ⊤ → Set where<br>> pt : P tt<br>><br>> test : (t : ⊤) → P t<br>> test t with t<br>> test t | tt = {!result!}<br>> where postulate result : P t<br>><br>> Note that result is not accepted despite the fact that it has exactly<br>> the declared type of test's result, which I believe is what you are<br>> seeing in your code as
well. The problem is that test's result type<br>> is changed when you do a with-match on t, by substituting tt for t. A<br>> solution is to replace your use of with by an explicit helper<br>> function, where you can tightly control exactly which occurrences of<br>> the with-scrutinee are replaced by the pattern:<br>> test₂ : (t : ⊤) → P t<br>> test₂ t = go t t<br>> where go : (t : ⊤) → (t' : ⊤) → P t<br>> go t tt = result<br>> where postulate result : P t<br>><br>> By the way, in your case, the occurrence of the with-scrutinee in the<br>> result type of your function is hidden by some calls, but Agda looks<br>> through this and I believe the problem is the same as what I've<br>> described above.<br>><br>> Regards<br>> Dominique<br>><br>><br>>
2013/3/5 Serge D. Mechveliani <<a ymailto="mailto:mechvel@botik.ru" href="mailto:mechvel@botik.ru">mechvel@botik.ru</a> <mailto:<a ymailto="mailto:mechvel@botik.ru" href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>>>:<br>> > On Sun, Mar 03, 2013 at 08:25:44AM +0100, Andreas Abel wrote:<br>> >> Sorry, I cannot explain this, because I cannot run your example<br>> >> (incomplete). --Andreas<br>> >><br>> ><br>> ><br>> > http://botik.ru/pub/local/Mechveliani/agdaNotes/rep.zip<br>> ><br>> > contains the precise Main.agda and readme.agda<br>> > (please, read first readme.agda).<br>> > I am sorry: the proggram is large.<br>> > I tried to present a small example, but have failed.<br>> > Of course, it can be reduced, say, 10 times, but this would need
a<br>> > considerable effort.<br>> > It looks like I am currently stuck in my attempt to write a library.<br>> ><br>> > Thank you in advance for help,<br>> ><br>> > -------<br>> > Sergei<br>> ><br>> ><br>> ><br>> >> On 02.03.13 10:43 AM, Serge D. Mechveliani wrote:<br>> >> >Dear all,<br>> >> >the attachement t.agda.zip<br>> >> ><br>> >> >contains a small code example where the same declaration of kind<br>> >> > postulate p : <signature><br>> >> >is taken in Agda-2.3.2 MAlonzo<br>> >> >as a correct type for p or not --
depending on whether p is set<br>> >> >directly after ` = ' or in the last branch for `with'.<br>> >> ><br>> >> >Can you, please, explain this?<br>> >> ><br>> >> ><br>> >> ><br>> >> >_______________________________________________<br>> >> >Agda mailing list<br>> >> ><a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<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>> >><br>> >> --<br>> >> Andreas Abel <><
Du bist der geliebte Mensch.<br>> >><br>> >> Theoretical Computer Science, University of Munich<br>> >> Oettingenstr. 67, D-80538 Munich, GERMANY<br>> >><br>> >> <a ymailto="mailto:andreas.abel@ifi.lmu.de" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a> <mailto:<a ymailto="mailto:andreas.abel@ifi.lmu.de" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>><br>> >> http://www2.tcs.ifi.lmu.de/~abel/<br>> >><br>> > _______________________________________________<br>> > Agda mailing list<br>> > <a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<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>> Agda mailing list<br>> <a ymailto="mailto:Agda@lists.chalmers.se" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a> <mailto:<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>><br>><br>><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><br>--
<br>Andreas Abel <>< Du bist der geliebte Mensch.<br><br>Theoretical Computer Science, University of Munich<br>Oettingenstr. 67, D-80538 Munich, GERMANY<br><br><a ymailto="mailto:andreas.abel@ifi.lmu.de" href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a><br><a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br><br><br> </div> </div> </div></body></html>