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

[Philip Wadler]

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

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Wed, 7 Jul 2021 at 10:18, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> This email was sent to you by someone outside the University.
> You should only click on links or attachments if you are certain that the
> email is genuine and the content is safe.
>
> I am using lhs2tex with agda mode which produces nice embedded latex code
> and also works for snippets in text.
>
> 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.
>
> Thorsten
>
> On 07/07/2021, 05:04, "Agda on behalf of Eduardo Ochs" <
> agda-bounces at lists.chalmers.se on behalf of eduardoochs at gmail.com> wrote:
>
>     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. =/
>
>       Thanks in advance!
>         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
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> _______________________________________________
> 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/1361f488/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210707/1361f488/attachment.ksh>