<div dir="ltr">I have an intern producing tooling to convert .lagda.md files to Latex. Agda's latex mode supports embedded code but makes snippets difficult, while markdown (.lagda.md) supports both. I will announce the tool here when it is complete, in about one month. Go well, -- P<div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, 7 Jul 2021 at 10:18, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">This email was sent to you by someone outside the University.<br>
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.<br>
<br>
I am using lhs2tex with agda mode which produces nice embedded latex code and also works for snippets in text.<br>
<br>
Agda can produce latex output for codde it has type checked but I find this is too inflexible and doesn't work well for snippets and examples.<br>
<br>
Thorsten<br>
<br>
On 07/07/2021, 05:04, "Agda on behalf of Eduardo Ochs" <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a> on behalf of <a href="mailto:eduardoochs@gmail.com" target="_blank">eduardoochs@gmail.com</a>> wrote:<br>
<br>
Hello list,<br>
<br>
how do I latex small snippets of Agda code?<br>
<br>
Ok, let me explain... I am a beginner with Agda and I am alternating<br>
between reading the tutorials and trying to understand the<br>
agda-categories library:<br>
<br>
<a href="https://github.com/agda/agda-categories" rel="noreferrer" target="_blank">https://github.com/agda/agda-categories</a><br>
<a href="https://arxiv.org/abs/2005.07059" rel="noreferrer" target="_blank">https://arxiv.org/abs/2005.07059</a><br>
<br>
I've been working on ways to visualize some statements and proofs in<br>
Category Theory and on ways to translate between different notations,<br>
and I would like to be able to add to a diagram like this one<br>
<br>
<a href="http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=33" rel="noreferrer" target="_blank">http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=33</a><br>
<br>
the information on how to translate each of my terms to Agda, using<br>
exactly the terminology of the agda-categories library whenever<br>
possible...<br>
<br>
My guess is that it should be possible to write a "poor man's way to<br>
typeset Agda source", like this thing here, that requires the user to<br>
add lots of backslashes by hand:<br>
<br>
% \co: a low-level way to typeset code; a poor man's "\verb"<br>
\def\co#1{{%<br>
\def\%{\char37}%<br>
\def\\{\char92}%<br>
\def\^{\char94}%<br>
\def\~{\char126}%<br>
\tt#1%<br>
}}<br>
\def\qco#1{`\co{#1}'}<br>
\def\qqco#1{``\co{#1}''}<br>
<br>
_and_ I guess that some people here may have written hacks like this,<br>
which is why I am asking... the tricky part is how to handle the<br>
unicode characters.<br>
<br>
By the way, I use lualatex most of the time and pdflatex when I need,<br>
and I've spent too much time learning how to use tricks like these<br>
<br>
\catcode`↗=13 \def↗{\nearrow} % lualatex<br>
\DeclareUnicodeCharacter{2198}{\searrow} % pdflatex<br>
<br>
and how to fix them when they break. =/<br>
<br>
Thanks in advance!<br>
Eduardo Ochs<br>
<a href="http://angg.twu.net/math-b.html" rel="noreferrer" target="_blank">http://angg.twu.net/math-b.html</a><br>
<a href="http://angg.twu.net/dednat6.html" rel="noreferrer" target="_blank">http://angg.twu.net/dednat6.html</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment.<br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored<br>
where permitted by law.<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>