<div dir="ltr">You can define showTerm yourself. The only annoying part is that fixity information is currently not available for names (see <a href="https://github.com/agda/agda/issues/1664">https://github.com/agda/agda/issues/1664</a>), so you would need to pretty print some superfluous parens.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jul 23, 2016 at 7:19 PM, Roman <span dir="ltr">&lt;<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi. `unquote` allows to print a Term, but it also performs type<br>
checking. Is there a way to print a Term just like `unquote` does, but<br>
without type checking it? I.e. something like `showTerm : Term -&gt;<br>
String`. It&#39;s hard to read plain Terms even with appropriate {-#<br>
DISPLAY #-} pragmas and more importantly we could define a type class<br>
<br>
record Quote {α} (A : Set α) : Set α where<br>
  field deepQuote : A -&gt; Term<br>
<br>
  show : A -&gt; String<br>
  show = showTerm ∘ deepQuote<br>
open Quote {{...}} public<br>
<br>
instead of the Show type class and delegate pretty printing to the<br>
built-in machinery therefore avoiding all the burden of dealing with<br>
associativity, inserting parentheses and spaces etc.<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>