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

[Thorsten Altenkirch]

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.