[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
> > I wish I were able to print my Agda code at different stages of
> > translation.
> Pretty printing for the Concrete syntax is defined in
> Agda.Syntax.Concrete.Pretty.  Abstract syntax can be pretty printed
> using Agda.Syntax.Abstract.Pretty.prettyA and Internal syntax with
> Agda.TypeChecking.Pretty.prettyTCM. 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.

Thanks! I will look into that.

-- 
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/20100428/f3e29371/attachment.bin