<div dir="ltr">The meta-level pretty printer prints things differently depending on what's in scope, so it couldn't be exposed as a pure function.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 2, 2016 at 11:28 AM, Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Sure, but Agda already knows how to pretty print terms, so why not<br>
exploit the existing machinery? By no means I could write as good<br>
pretty printer as Agda already has. Or is it not that straightforward<br>
to give access to the meta-level pretty printer?<br>
</blockquote></div><br></div>