<br><div class="gmail_quote">On Mon, May 17, 2010 at 8:55 PM, David Haguenauer <span dir="ltr">&lt;<a href="mailto:haguenad@iro.umontreal.ca">haguenad@iro.umontreal.ca</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">* Ulf Norell &lt;<a href="mailto:ulfn@chalmers.se">ulfn@chalmers.se</a>&gt;, 2010-04-27 21:24:20 Tue:<br>
</div><div class="im">&gt; On Tue, Apr 27, 2010 at 9:07 PM, David Haguenauer &lt;<a href="mailto:haguenad@iro.umontreal.ca">haguenad@iro.umontreal.ca</a><br>
&gt; &gt; wrote:<br>
</div>&gt; &gt; [...] I wish I were able to print my Agda code at different stages of<br>
&gt; &gt; translation.<br>
&gt;<br>
&gt; [...] The pretty printers for Abstract and Internal syntax run in<br>
<div class="im">&gt; the type checking monad, since they use the current scope to figure<br>
&gt; out how to print things.<br>
<br>
</div>As a followup question: I&#39;m attempting to pretty-print from within<br>
module ConcreteToAbstract, in function concreteToAbstract (because<br>
that seemed to be a good place). I can&#39;t really tell how to get a TCM<br>
there; is there a way to get a (possibly dummy) one, or should I print<br>
from somewhere else?<br></blockquote><div><br></div><div>The scope monad used by concreteToAbstract is actually TCM, so you</div><div>can just call TCM functions as they are.</div><div><br></div><div>/ Ulf</div></div>