<br><div class="gmail_quote">On Mon, May 17, 2010 at 8:55 PM, David Haguenauer <span dir="ltr"><<a href="mailto:haguenad@iro.umontreal.ca">haguenad@iro.umontreal.ca</a>></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 <<a href="mailto:ulfn@chalmers.se">ulfn@chalmers.se</a>>, 2010-04-27 21:24:20 Tue:<br>
</div><div class="im">> On Tue, Apr 27, 2010 at 9:07 PM, David Haguenauer <<a href="mailto:haguenad@iro.umontreal.ca">haguenad@iro.umontreal.ca</a><br>
> > wrote:<br>
</div>> > [...] I wish I were able to print my Agda code at different stages of<br>
> > translation.<br>
><br>
> [...] The pretty printers for Abstract and Internal syntax run in<br>
<div class="im">> the type checking monad, since they use the current scope to figure<br>
> out how to print things.<br>
<br>
</div>As a followup question: I'm attempting to pretty-print from within<br>
module ConcreteToAbstract, in function concreteToAbstract (because<br>
that seemed to be a good place). I can'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>