[Agda] goal normalization request

[Darryl]

Aha! So in fact this is already implemented. Goes to show, I should rely on the docs more. :)
 
- darryl


________________________________
 From: Nils Anders Danielsson <nad at chalmers.se>
To: Darryl <psygnisfive at yahoo.com> 
Cc: "agda at lists.chalmers.se" <agda at lists.chalmers.se> 
Sent: Thursday, December 13, 2012 2:43 AM
Subject: Re: [Agda] goal normalization request
 
On 2012-12-12 19:28, Darryl wrote:
> In emacs, goals don't normalize when they're all being displayed at
> once (i.e. when no goal is currently in focus), but when one is in
> focus, it only shows up normalized.

Not necessarily:

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations

-- /NAD
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121213/83a4cf81/attachment.html