[Agda] How to show a Term?

Ulf Norell ulf.norell at gmail.com
Tue Aug 2 11:36:35 CEST 2016


The meta-level pretty printer prints things differently depending on what's
in scope, so it couldn't be exposed as a pure function.

/ Ulf

On Tue, Aug 2, 2016 at 11:28 AM, Roman <effectfully at gmail.com> wrote:

> Sure, but Agda already knows how to pretty print terms, so why not
> exploit the existing machinery? By no means I could write as good
> pretty printer as Agda already has. Or is it not that straightforward
> to give access to the meta-level pretty printer?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160802/38940fa5/attachment.html


More information about the Agda mailing list