[Agda] can normal forms be made to look shorter somehow?

[Ulf Norell]

On Thu, May 8, 2008 at 5:00 PM, Samuel Bronson <naesten at gmail.com> wrote:

> Computing the normal form of "list'" in the attached module generates
> a large output. I reported the fact that the Fin constructors were
> being printed qualified at this URL:
>    http://code.google.com/p/agda/issues/detail?id=69
> but I'm wondering if there is anything else that could be done to make
> Fins display shorter? For instance, displaying them in some form other
> than unary might be nice. Any ideas?


I suppose you could define a "presentation" version of Gen where you replace
the Fins by natural numbers, and then convert into the presentation form
before you print it. Closed natural numbers are printed on decimal form.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080508/76c39a1b/attachment.html