[Agda] goal normalization request

Darryl psygnisfive at yahoo.com
Thu Dec 13 21:24:44 CET 2012

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:


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

More information about the Agda mailing list