% This file:
%   http://angg.twu.net/LATEX/2022Cats5.lagda.tex.html
%   http://angg.twu.net/LATEX/2022Cats5.lagda.tex
%           (find-angg "LATEX/2022Cats5.lagda.tex")
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% (find-LATEX "2022Cats5.lagda.tex")
% (defun c  () (interactive) (eec-agdalatex-sh "2022Cats5" "-record" :end))
% (defun C  () (interactive) (eec-agdalatex-sh "2022Cats5" "" "Success!!!"))
% (defun D  () (interactive) (find-pdf-page      "~/LATEX/2022Cats5.pdf"))
% (defun d  () (interactive) (find-pdftools-page "~/LATEX/2022Cats5.pdf"))
% (defun e  () (interactive) (find-angg "LATEX/2022Cats5.lagda.tex"))
% (defun et () (interactive) (find-angg "LATEX/2022Cats5.tex"))
% (defun a  () (interactive) (find-angg  "AGDA/2022Cats5.agda"))
% (defun u  () (interactive) (find-latex-upload-links "2022Cats5"))
% (defun v  () (interactive) (find-2a '(e) '(d)))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (defun d0 () (interactive) (find-ebuffer "2022Cats5.pdf"))
%          (code-eec-LATEX "2022Cats5")
%
% (defun e  () (interactive) (find-LATEX "2022Cats5.lagda.tex"))
% (defun et () (interactive) (find-LATEX "2022Cats5.tex"))
% (defun v () (interactive) (find-pdftoolsr-page "~/LATEX/2022Cats5.pdf"))
% (find-2a nil '(find-LATEX "2022template.lagda.tex"))
% (find-agdalatex-links "2022Cats5")
% (find-agdafile-links  "2022Cats5")
% (find-lualatex-links  "2022Cats5")

% (defun e () (interactive) (find-LATEX "2022Cats5.lagda.tex"))
% (defun v () (interactive) (find-pdftoolsr-page "~/LATEX/2022Cats5.pdf"))
% (find-2a nil '(find-LATEX "2022template.lagda.tex"))
% (find-agdalatex-links "2022Cats5")


\documentclass{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%
\usepackage{proof}   % For derivation trees ("%:" lines)
\input diagxy        % For 2D diagrams ("%D" lines)
\xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx21}               % (find-LATEX "edrx21.sty")
\input edrxaccents.tex            % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex            % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex           % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
\usepackage{agda}                 % (find-LATEX "agda.sty")
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

\catcode`₀=13 \def₀{{\ensuremath{{}_0}}}
\catcode`₁=13 \def₁{{\ensuremath{{}_1}}}
\catcode`₂=13 \def₂{{\ensuremath{{}_2}}}
\catcode`₃=13 \def₃{{\ensuremath{{}_3}}}

\begin{code}
module 2022Cats5 where
\end{code}

\GenericWarning{Success:}{Success!!!}  % Used by `M-x cv'

\end{document}

* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
agda --latex --latex-dir=. 2022Cats5.lagda.tex
laf 2022Cats5*
cd ~/LATEX/
lualatex 2022Cats5.tex

% (find-fline "~/AGDA/latex/")
% (find-fline "~/AGDA/latex/Logic2.tex")

% (find-agdausermanualpage (+ 4 195) "4.7 Generating LaTeX")
% (find-agdausermanualtext (+ 4 195) "4.7 Generating LaTeX")
% (find-agdausermanualpage (+ 4 95) "3.19.3 Literate Agda")
% (find-agdausermanualtext (+ 4 95) "3.19.3 Literate Agda")

% Local Variables:
% coding:  utf-8-unix
% modes:   (latex-mode agda2-mode)
% End: