[Agda] Printing strings in the emacs mode

[Setzer A.G.]

If your output is actually a string, you could create an interactive program and let it print it out for you.
The ooAgda library https://github.com/agda/ooAgda  has in examples/consoleExamples currently three  simple examples of console programs (more to come soon ...)  See READMEconsolePrograms.txt

Anton
________________________________________
From: Agda [agda-bounces at lists.chalmers.se] on behalf of Guillaume Brunerie [guillaume.brunerie at gmail.com]
Sent: 21 November 2017 02:37
To: agda list
Subject: [Agda] Printing strings in the emacs mode

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
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda