<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hi, </div><div><br></div><div>to be precise: I expected that the insertion of f happens automatically</div><div>when I started the refinement. It works when I insert f manually.</div><div><br></div><div>Is there an example where the refinement gives me some</div><div>information that is difficult to figure out myself?</div><div><br></div><div>Best regards</div><div><br></div><br><div><div>On 29 Sep 2009, at 17:06, Christoph Herrmann wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Hi,</div><div><br></div><div>I have doubts that my emacs installation with Agda is working correctly, </div><div>so I tried a given example.</div><div><br></div><div>I found on one lecture slide of Anton Setzer</div><div><span class="Apple-style-span" style="font-size: 12px; ">CS 336/CS M36 (part 2)/CS M46 Interactive Theorem Proving, Lent Term 2008, Sec. 3 (c)<span style="font: 16.9px Helvetica">3-93:</span></span></div><div><font class="Apple-style-span" color="#FF4000" face="Times" size="4"><span class="Apple-style-span" style="font-size: 14px;"><br></span></font></div><div><span style="font: 16.9px Helvetica"><span class="Apple-style-span" style="color: rgb(255, 64, 0); font-family: Times; "><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">postulate </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">A </span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">: Set </span></font></span></span></div><div><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 24.8px/normal Times; color: rgb(255, 64, 0); "><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">postulate </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">B </span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">: Set </span></font></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 24.8px/normal Times; color: rgb(255, 64, 0); "><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">postulate </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">f </span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">: </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">A → B </span></font></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 24.8px/normal Times; color: rgb(255, 64, 0); "><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;"><span style="font: 24.8px Helvetica"></span>postulate </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">a </span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">: </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">A </span></font></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 24.8px/normal Times; color: rgb(255, 64, 0); "><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">b </span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">: </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">B</span></font></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 25.6px/normal Helvetica; "><span style="font: 24.8px Helvetica; color: #ff4000"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">b </span></font></span><span style="font: 24.8px Times; color: #ff4000"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">= </span></font></span><span style="font: 24.8px Helvetica; color: #ff4000"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">{</span></font></span><span style="font: 24.8px Times; color: #ff4000"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">! !</span></font></span><span style="font: 24.8px Helvetica; color: #ff4000"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">} </span></font></span></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 25.6px/normal Helvetica; "><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;"><br></span></font></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 25.6px/normal Helvetica; "><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;"><span style="font: 24.8px Helvetica; color: #ff4000"></span>Then we can insert </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">f </span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">into this goal and use menu</span></font></div><div style="margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margin-left: 0px; font: normal normal normal 25.6px/normal Helvetica; color: rgb(0, 52, 255); "><b><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">Refine (C-c C-r)</span></font></b></div><div><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">The system shows </span></font><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">b </span></font></span><span style="font: 24.8px Times"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">= </span></font></span><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">f {</span></font></span><span style="font: 24.8px Times"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">! !</span></font></span><span style="font: 24.8px Helvetica"><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">}</span></font></span><font class="Apple-style-span" size="4"><span class="Apple-style-span" style="font-size: 14px;">.</span></font></div><div>---------------------------------------------------------</div><div>Unfortunately, this does not work for me. After loading the file the hole is replaced by </div><div>b = { }0</div><div>Placing the cursor inside the { } and selecting refinement the refinement does not </div><div>happen visibly for me, but I'm asked for a number of a goal. I typed 0 but the goal</div><div>did not change to the result as on the slides.</div><div><br></div><div>Is there an easy way to check what the reason could be; e.g., the values of</div><div>environment variables in emacs (I'm using Aquamacs on MacOSX)?</div><div><br></div><div>The type inference in simple cases seems to work, although I'm not getting</div><div>the normal form displayed.</div><div><br></div><div>Many thanks in advance</div><div>-- </div><div> Dr. Christoph Herrmann</div><div> University of St Andrews, Scotland/UK</div><div> phone: office: +44 1334 461629, home: +44 1334 478648 </div><div> email: <a href="mailto:ch@cs.st-andrews.ac.uk">ch@cs.st-andrews.ac.uk</a>, <a href="mailto:c.herrmann@virgin.net">c.herrmann@virgin.net</a></div><div> URL: <a href="http://www.cs.st-andrews.ac.uk/~ch">http://www.cs.st-andrews.ac.uk/~ch</a></div><div> </div><div> The University of St Andrews is a charity registered in Scotland: No SC013532</div><div><br></div></div></div><br class="Apple-interchange-newline"><br class="Apple-interchange-newline">
</div>
<br></div>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br><div>
<span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><div>--</div><div> Dr. Christoph Herrmann</div><div> University of St Andrews, Scotland/UK</div><div> phone: office: +44 1334 461629, home: +44 1334 478648 </div><div> email: <a href="mailto:ch@cs.st-andrews.ac.uk">ch@cs.st-andrews.ac.uk</a>, <a href="mailto:c.herrmann@virgin.net">c.herrmann@virgin.net</a></div><div> URL: <a href="http://www.cs.st-andrews.ac.uk/~ch">http://www.cs.st-andrews.ac.uk/~ch</a></div><div> </div><div> The University of St Andrews is a charity registered in Scotland: No SC013532</div><div><br></div></div></div></span><br class="Apple-interchange-newline"></span><br class="Apple-interchange-newline">
</div>
<br></body></html>