[Agda] Printing strings in the emacs mode

[Guillaume Brunerie]

Hi all,

I’m using an Agda program to generate some Agda code. I’m not using
reflection, I’m just using Agda as a regular functional programming
language to generate strings, that I then want to copy-paste in a
different file.

For now, I didn’t bother with compilation, so I’m just defining terms
of type String (from the standard library), and then I use C-c C-n in
order to get their normal form.

My problem is that in the result of C-c C-n, the string is surrounded
by quotes, and the new lines are escaped as \n, which makes it a bit
annoying to copy-paste, as I have to do a search and replace
afterwards.

Is there a way to use something like C-c C-n in order to get the
normal form of a term of type String, but have it printed properly,
without escaping the new lines and without the quotes before and
after?

Thanks,
Best,
Guillaume