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

Jason Hu fdhzs2010 at hotmail.com
Wed Jul 7 06:09:24 CEST 2021

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.

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

From: Eduardo Ochs<mailto:eduardoochs at gmail.com>
Sent: Wednesday, July 7, 2021 12:04 AM
To: agda at lists.chalmers.se<mailto:agda at lists.chalmers.se>
Subject: [Agda] Poor man's way to latex Agda source

Hello list,

how do I latex small snippets of Agda code?

Ok, let me explain... I am a beginner with Agda and I am alternating
between reading the tutorials and trying to understand the
agda-categories library:

https://github.com/agda/agda-categories
https://arxiv.org/abs/2005.07059

I've been working on ways to visualize some statements and proofs in
Category Theory and on ways to translate between different notations,
and I would like to be able to add to a diagram like this one

http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=33

the information on how to translate each of my terms to Agda, using
exactly the terminology of the agda-categories library whenever
possible...

My guess is that it should be possible to write a "poor man's way to
typeset Agda source", like this thing here, that requires the user to
add lots of backslashes by hand:

% \co: a low-level way to typeset code; a poor man's "\verb"
\def\co#1{{%
\def\%{\char37}%
\def\\{\char92}%
\def\^{\char94}%
\def\~{\char126}%
\tt#1%
}}
\def\qco#1{\co{#1}'}
\def\qqco#1{\co{#1}''}

_and_ I guess that some people here may have written hacks like this,
which is why I am asking... the tricky part is how to handle the
unicode characters.

By the way, I use lualatex most of the time and pdflatex when I need,
and I've spent too much time learning how to use tricks like these

\catcode↗=13 \def↗{\nearrow} % lualatex
\DeclareUnicodeCharacter{2198}{\searrow} % pdflatex

and how to fix them when they break. =/

Eduardo Ochs
http://angg.twu.net/math-b.html
http://angg.twu.net/dednat6.html
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210707/2a9857aa/attachment.html>