[Agda] Adding "print" to TC monad?

[Jon Sterling]

Hi all,

I am starting to learn to use Agda's excellent reflection facilities /
TC monad to implement some proof automation, and I have been thinking
that it would be very useful to have a way to do "printf"-style
debugging in elaborator scripts. Right now, I can kind of simulate this
by throwing an error, but I would like to be able to print information
without aborting the proof.

Does anybody have any thoughts about adding another operation to the TC
monad for printing (i.e. whether this is a good idea)? If people think
this sounds like a good idea, I would probably be willing to do the
hacking and submit a pull request.

Best wishes,
Jon