[Agda] Poor man's way to latex Agda source

[Eduardo Ochs]

On Wed, 7 Jul 2021 at 01:09, Jason Hu <fdhzs2010 at hotmail.com> wrote:
>
> I am still not sure what exactly you are looking for. What I do is I
> use minted to typeset the code, and I just copy and paste the code
> in. other packages, of course, would also work.

I'll try to do that!

> Or are you asking how to handle the Unicode used in an Agda source?

I guess that minted handles it in the right way, and I'll probably be
able to learn what I need by studying its output. Minted is not
mentioned in the Agda User Manual, and I was looking for pointers...

  Thanks!!! =)
    Eduardo