Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% 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: