[Agda] goal normalization request

Andreas Abel andreas.abel at ifi.lmu.de
Thu Dec 13 01:39:59 CET 2012

True.  See also:


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

More information about the Agda mailing list