<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Aha! So in fact this is already implemented. Goes to show, I should rely on the docs more. :)</span></div><div></div><div> </div><div>- darryl<br></div> <div style="font-size: 10pt; font-family: arial, helvetica, sans-serif; "> <div style="font-size: 12pt; font-family: 'times new roman', 'new york', times, serif; "> <div dir="ltr"> <font size="2" face="Arial"> <hr size="1"> <b><span style="font-weight:bold;">From:</span></b> Nils Anders Danielsson <nad@chalmers.se><br> <b><span style="font-weight: bold;">To:</span></b> Darryl <psygnisfive@yahoo.com> <br><b><span style="font-weight: bold;">Cc:</span></b> "agda@lists.chalmers.se" <agda@lists.chalmers.se> <br> <b><span style="font-weight: bold;">Sent:</span></b> Thursday, December 13, 2012 2:43 AM<br> <b><span style="font-weight: bold;">Subject:</span></b>
Re: [Agda] goal normalization request<br> </font> </div> <br>
On 2012-12-12 19:28, Darryl wrote:<br>> In emacs, goals don't normalize when they're all being displayed at<br>> once (i.e. when no goal is currently in focus), but when one is in<br>> focus, it only shows up normalized.<br><br>Not necessarily:<br><br> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations<br><br>-- /NAD<br><br><br> </div> </div> </div></body></html>