[Agda] goal normalization request

[Andreas Abel]

True.  See also:

   http://code.google.com/p/agda/issues/detail?id=734

On 12.12.12 7:28 PM, 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. It would be incredibly useful if the focused
> goal showed up as un-normalized, and could be normalized, or possibly
> stepped, so that users can control how much normalization they see. This
> would be especially useful because it would eliminate the need for
> certain wrapper types that exist only to prevent normalization.
>
> - darryl mcadams
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/