UlfNorell
commented
10 years ago From stevan.a...@gmail.com on November 27, 2013 10:20:14
Argh, this amended patch has the correct filename for the test case.
Attachment: agda-latex-backend-agdaindent2.patch
From stevan.a...@gmail.com on November 27, 2013 19:15:30
For some reason I can't explain the following code:
\documentclass{article}
\usepackage{agda}
\begin{document}
%\renewcommand{\AgdaIndent}{\;\;}
\begin{code} record Sigma (A : Set) (B : A → Set) : Set where constructor , field proj₁ : A proj₂ : B proj₁
open Sigma public \end{code}
\begin{code} uncurry : {A : Set} {B : A → Set} {C : Sigma A B → Set} → ((x : A) → (y : B x) → C (x , y)) → ((p : Sigma A B) → C p) uncurry f (x , y) = f x y \end{code}
\end{document}
Does not compile with the old \;\; value of \AgdaIndent. Changing it to $\;\;$ fixes this.
The attached patch changes \AgdaIndent in agda.sty and adds the above test case to the test suite.
Attachment: agda-latex-backend-agdaindent.patch
Original issue: http://code.google.com/p/agda/issues/detail?id=982