Open WhatisRT opened 1 month ago
Here is a version without the standard library:
\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{AgdaMultiCode}
\begin{code}
case_of_ : {A B : Set} (a : A) (f : A → B) → B
case a of f = f a
open import Agda.Builtin.Bool -- needed in this block before the ff
ff : Bool
ff = true
where
f1 : Bool
f1 = case true of
\end{code}
\begin{code}[hide]
λ where
\end{code}
\begin{code}
_ → true
f2 : Bool
f2 = case true of
\end{code}
\begin{code}[hide]
λ where
\end{code}
\begin{code}
_ → true
\end{code}
\end{AgdaMultiCode}
\end{document}
It does not depend on -xelatex
.
Shrank the generated latex file to this:
\documentclass{article}
\usepackage{agda}
\begin{document}
\begin{AgdaMultiCode}
%% The column names must be different, e.g foo/bar/baz
\begin{code}
\\ %% needed
\>[foo]
\end{code}
\begin{code}
\>[bar]
\end{code}
\begin{code}
\>[baz]
\end{code}
\end{AgdaMultiCode}
\end{document}
The AgdaMultiCode
environment can be removed by declaring \setboolean{Agda@Align}{true}
instead.
Shrinking away agda.sty
I arrive at this polytable
reproducer (still same error):
\documentclass{article}
\RequirePackage{polytable}
\defaultcolumn{l}
\begin{document}
%% The column names must be different
\begin{pboxed}\savecolumns
\\ %% needed
\>[foo]
\end{pboxed}
\begin{pboxed}\restorecolumns
\>[bar]
\end{pboxed}
\begin{pboxed}\restorecolumns
\>[baz]
\end{pboxed}
\end{document}
This might be an issue in polytable
rather than in agda.sty
. I reported this upstream:
Here's a literate Agda file that LaTeX doesn't like:
Changing pretty much anything will make this not fail. For example renaming
ff
tof
or indenting the last line off3
(_ → true
) by two more spaces. Even the two[hide]
modifiers cannot be removed.The sequence of commands I'm using to compile this is:
The error message I'm getting is the following: