[Agda] Debugging Agda's syntaxes

[David Haguenauer]

* Ulf Norell <ulfn at chalmers.se>, 2010-04-27 21:24:20 Tue:
> On Tue, Apr 27, 2010 at 9:07 PM, David Haguenauer <haguenad at iro.umontreal.ca
> > wrote:
> > [...] I wish I were able to print my Agda code at different stages of
> > translation.
>
> [...] The pretty printers for Abstract and Internal syntax run in
> the type checking monad, since they use the current scope to figure
> out how to print things.

As a followup question: I'm attempting to pretty-print from within
module ConcreteToAbstract, in function concreteToAbstract (because
that seemed to be a good place). I can't really tell how to get a TCM
there; is there a way to get a (possibly dummy) one, or should I print
from somewhere else?

-- 
Thanks,
David Haguenauer
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 254 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100517/68bccbcf/attachment.bin