Agda-2.6.4: src/data/latex/agda.sty
% ----------------------------------------------------------------------
% Some useful commands when doing highlighting of Agda code in LaTeX.
% ----------------------------------------------------------------------
% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
% !!! NOTE: when you make changes to this file, bump the date. !!!
% !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
\ProvidesPackage{agda}
[2021/07/14 version 2.6.4 Formatting LaTeX generated by Agda]
\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
calc, environ, xparse, xkeyval}
% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation
\newif\ifxetexorluatex
\ifxetex
\xetexorluatextrue
\else
\ifluatex
\xetexorluatextrue
\else
\xetexorluatexfalse
\fi
\fi
% ----------------------------------------------------------------------
% Options
\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}}
\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}
\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
\DeclareOption{references}{
\@AgdaEnableReferencestrue
}
\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
\DeclareOption{links}{
\@AgdaEnableLinkstrue
}
\ProcessOptions\relax
% ----------------------------------------------------------------------
% Font setup
\tracinglostchars=2 % If the font is missing some symbol, then say
% so in the compilation output.
% ----------------------------------------------------------------------
% Colour schemes.
\providecommand{\AgdaColourScheme}{standard}
% ----------------------------------------------------------------------
% References to code (needs additional post-processing of tex files to
% work, see wiki for details).
\if@AgdaEnableReferences
\RequirePackage{catchfilebetweentags, xstring}
\newcommand{\AgdaRef}[2][]{%
\StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%
\ifthenelse{\isempty{#1}}%
{\ExecuteMetaData{AgdaTag-\tmp}}%
{\ExecuteMetaData{#1}{AgdaTag-\tmp}}
}
\fi
\providecommand{\AgdaRef}[2][]{#2}
% ----------------------------------------------------------------------
% Links (only done if the option is passed and the user has loaded the
% hyperref package).
\if@AgdaEnableLinks
\@ifpackageloaded{hyperref}{
% List that holds added targets.
\newcommand{\AgdaList}[0]{}
\newtoggle{AgdaIsElem}
\newcounter{AgdaIndex}
\newcommand{\AgdaLookup}[3]{%
\togglefalse{AgdaIsElem}%
\setcounter{AgdaIndex}{0}%
\renewcommand*{\do}[1]{%
\ifstrequal{#1}{##1}%
{\toggletrue{AgdaIsElem}\listbreak}%
{\stepcounter{AgdaIndex}}}%
\dolistloop{\AgdaList}%
\iftoggle{AgdaIsElem}{#2}{#3}%
}
\newcommand*{\AgdaTargetHelper}[1]{%
\AgdaLookup{#1}%
{\PackageError{agda}{``#1'' used as target more than once}%
{Overloaded identifiers and links do not%
work well, consider using unique%
\MessageBreak identifiers instead.}%
}%
{\listadd{\AgdaList}{#1}%
\hypertarget{Agda\theAgdaIndex}{}%
}%
}
\newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}
\newcommand{\AgdaLink}[1]{%
\AgdaLookup{#1}%
{\hyperlink{Agda\theAgdaIndex}{#1}}%
{#1}%
}
}{\PackageError{agda}{Load the hyperref package before the agda package}{}}
\fi
\providecommand{\AgdaTarget}[1]{}
\providecommand{\AgdaLink}[1]{#1}
% ----------------------------------------------------------------------
% Font styles.
\newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
\newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
}{
\newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
}
\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
% ----------------------------------------------------------------------
% Colours.
% ----------------------------------
% The black and white colour scheme.
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
% Aspect colours.
\definecolor{AgdaComment} {HTML}{000000}
\definecolor{AgdaPragma} {HTML}{000000}
\definecolor{AgdaKeyword} {HTML}{000000}
\definecolor{AgdaString} {HTML}{000000}
\definecolor{AgdaNumber} {HTML}{000000}
\definecolor{AgdaSymbol} {HTML}{000000}
\definecolor{AgdaPrimitiveType}{HTML}{000000}
% NameKind colours.
\definecolor{AgdaBound} {HTML}{000000}
\definecolor{AgdaGeneralizable} {HTML}{000000}
\definecolor{AgdaInductiveConstructor} {HTML}{000000}
\definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
\definecolor{AgdaDatatype} {HTML}{000000}
\definecolor{AgdaField} {HTML}{000000}
\definecolor{AgdaFunction} {HTML}{000000}
\definecolor{AgdaMacro} {HTML}{000000}
\definecolor{AgdaModule} {HTML}{000000}
\definecolor{AgdaPostulate} {HTML}{000000}
\definecolor{AgdaPrimitive} {HTML}{000000}
\definecolor{AgdaRecord} {HTML}{000000}
\definecolor{AgdaArgument} {HTML}{000000}
% Other aspect colours.
\definecolor{AgdaDottedPattern} {HTML}{000000}
\definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3}
\definecolor{AgdaUnsolvedConstraint}{HTML}{D3D3D3}
\definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
\definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
\definecolor{AgdaErrorWarning} {HTML}{BEBEBE}
\definecolor{AgdaError} {HTML}{696969}
% Misc.
\definecolor{AgdaHole} {HTML}{BEBEBE}
% ----------------------------------
% Conor McBride's colour scheme.
}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
% Aspect colours.
\definecolor{AgdaComment} {HTML}{B22222}
\definecolor{AgdaPragma} {HTML}{000000}
\definecolor{AgdaKeyword} {HTML}{000000}
\definecolor{AgdaString} {HTML}{000000}
\definecolor{AgdaNumber} {HTML}{000000}
\definecolor{AgdaSymbol} {HTML}{000000}
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
% NameKind colours.
\definecolor{AgdaBound} {HTML}{A020F0}
\definecolor{AgdaGeneralizable} {HTML}{A020F0}
\definecolor{AgdaInductiveConstructor} {HTML}{8B0000}
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
\definecolor{AgdaDatatype} {HTML}{0000CD}
\definecolor{AgdaField} {HTML}{8B0000}
\definecolor{AgdaFunction} {HTML}{006400}
\definecolor{AgdaMacro} {HTML}{006400}
\definecolor{AgdaModule} {HTML}{006400}
\definecolor{AgdaPostulate} {HTML}{006400}
\definecolor{AgdaPrimitive} {HTML}{006400}
\definecolor{AgdaRecord} {HTML}{0000CD}
\definecolor{AgdaArgument} {HTML}{404040}
% Other aspect colours.
\definecolor{AgdaDottedPattern} {HTML}{000000}
\definecolor{AgdaUnsolvedMeta} {HTML}{FFD700}
\definecolor{AgdaUnsolvedConstraint}{HTML}{FFD700}
\definecolor{AgdaTerminationProblem}{HTML}{FF0000}
\definecolor{AgdaIncompletePattern} {HTML}{A020F0}
\definecolor{AgdaErrorWarning} {HTML}{FF0000}
\definecolor{AgdaError} {HTML}{F4A460}
% Misc.
\definecolor{AgdaHole} {HTML}{9DFF9D}
% ----------------------------------
% The standard colour scheme.
}{
% Aspect colours.
\definecolor{AgdaComment} {HTML}{B22222}
\definecolor{AgdaPragma} {HTML}{000000}
\definecolor{AgdaKeyword} {HTML}{CD6600}
\definecolor{AgdaString} {HTML}{B22222}
\definecolor{AgdaNumber} {HTML}{A020F0}
\definecolor{AgdaSymbol} {HTML}{404040}
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
% NameKind colours.
\definecolor{AgdaBound} {HTML}{000000}
\definecolor{AgdaGeneralizable} {HTML}{000000}
\definecolor{AgdaInductiveConstructor} {HTML}{008B00}
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
\definecolor{AgdaDatatype} {HTML}{0000CD}
\definecolor{AgdaField} {HTML}{EE1289}
\definecolor{AgdaFunction} {HTML}{0000CD}
\definecolor{AgdaMacro} {HTML}{458B74}
\definecolor{AgdaModule} {HTML}{A020F0}
\definecolor{AgdaPostulate} {HTML}{0000CD}
\definecolor{AgdaPrimitive} {HTML}{0000CD}
\definecolor{AgdaRecord} {HTML}{0000CD}
\definecolor{AgdaArgument} {HTML}{404040}
% Other aspect colours.
\definecolor{AgdaDottedPattern} {HTML}{000000}
\definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00}
\definecolor{AgdaUnsolvedConstraint}{HTML}{FFFF00}
\definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
\definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
\definecolor{AgdaErrorWarning} {HTML}{FFA07A}
\definecolor{AgdaError} {HTML}{FF0000}
% Misc.
\definecolor{AgdaHole} {HTML}{9DFF9D}
}}
% ----------------------------------------------------------------------
% Commands.
\newcommand{\AgdaNoSpaceMath}[1]
{\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}
% Aspect commands.
\newcommand{\AgdaComment} [1]
{\AgdaNoSpaceMath{\textcolor{AgdaComment}{\AgdaCommentFontStyle{#1}}}}
\newcommand{\AgdaPragma} [1]
{\AgdaNoSpaceMath{\textcolor{AgdaPragma}{\AgdaCommentFontStyle{#1}}}}
\newcommand{\AgdaKeyword} [1]
{\AgdaNoSpaceMath{\textcolor{AgdaKeyword}{\AgdaKeywordFontStyle{#1}}}}
\newcommand{\AgdaString} [1]
{\AgdaNoSpaceMath{\textcolor{AgdaString}{\AgdaStringFontStyle{#1}}}}
\newcommand{\AgdaNumber} [1]
{\AgdaNoSpaceMath{\textcolor{AgdaNumber}{\AgdaFontStyle{#1}}}}
\newcommand{\AgdaSymbol} [1]
{\AgdaNoSpaceMath{\textcolor{AgdaSymbol}{\AgdaFontStyle{#1}}}}
\newcommand{\AgdaPrimitiveType}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaPrimitiveType}{\AgdaFontStyle{#1}}}}
%% Andreas, 2021-07-14, issue #5471
%% To make italics correction \/ work, the font-style modifier
%% needs to be inside, in particular inside the \textcolor modifier,
%% as the \textcolor{} wrapping around something hides its content
%% to the logic that resolves \/ into a space or not.
% Note that, in code generated by the LaTeX backend, \AgdaOperator is
% always applied to a NameKind command.
\newcommand{\AgdaOperator} [1]{#1}
% NameKind commands.
% The user can control the typesetting of (certain) individual tokens
% by redefining the following command. The first argument is the token
% and the second argument the thing to be typeset (sometimes just the
% token, sometimes \AgdaLink{<the token>}). Example:
%
% \usepackage{ifthen}
%
% % Insert extra space before some tokens.
% \DeclareRobustCommand{\AgdaFormat}[2]{%
% \ifthenelse{
% \equal{#1}{≡⟨} \OR
% \equal{#1}{≡⟨⟩} \OR
% \equal{#1}{∎}
% }{\ }{}#2}
%
% Note the use of \DeclareRobustCommand.
\newcommand{\AgdaFormat}[2]{#2}
\newcommand{\AgdaBound}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaBound}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}}
\newcommand{\AgdaGeneralizable}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaGeneralizable}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}}
\newcommand{\AgdaInductiveConstructor}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaInductiveConstructor}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaCoinductiveConstructor}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaCoinductiveConstructor}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaDatatype}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaDatatype}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaField}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaField}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaFunction}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaFunction}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaMacro}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaMacro}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaModule}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaModule}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaPostulate}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaPostulate}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaPrimitive}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaPrimitive}{\AgdaFontStyle{\AgdaFormat{#1}{#1}}}}}
\newcommand{\AgdaRecord}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaRecord}{\AgdaFontStyle{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
\newcommand{\AgdaArgument}[1]
{\AgdaNoSpaceMath{\textcolor{AgdaArgument}{\AgdaBoundFontStyle{\AgdaFormat{#1}{#1}}}}}
% Other aspect commands.
\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}}
\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}}
\newcommand{\AgdaUnsolvedMeta} [1]
{\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
\newcommand{\AgdaUnsolvedConstraint}[1]
{\AgdaFontStyle{\colorbox{AgdaUnsolvedConstraint}{#1}}}
\newcommand{\AgdaTerminationProblem}[1]
{\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
\newcommand{\AgdaErrorWarning} [1]{\colorbox{AgdaErrorWarning}{#1}}
\newcommand{\AgdaError} [1]
{\textcolor{AgdaError}{\AgdaFontStyle{\underline{#1}}}}
\newcommand{\AgdaCatchallClause} [1]{#1} % feel free to change this
% Used to hide code from LaTeX.
%
% Note that this macro has been deprecated in favour of giving the
% hide argument to the code environment.
\long\def\AgdaHide#1{\ignorespaces}
% Misc.
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
% ----------------------------------------------------------------------
% The code environment.
\newcommand{\AgdaCodeStyle}{}
% \newcommand{\AgdaCodeStyle}{\tiny}
\ifdefined\mathindent
{}
\else
\newdimen\mathindent\mathindent\leftmargini
\fi
% Adds the given amount of vertical space and starts a new line.
%
% The implementation comes from lhs2TeX's polycode.fmt, written by
% Andres Löh.
\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%
{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
% Should there be space around code?
\newboolean{Agda@SpaceAroundCode}
% Use this command to avoid extra space around code blocks.
\newcommand{\AgdaNoSpaceAroundCode}{%
\setboolean{Agda@SpaceAroundCode}{false}}
% Use this command to include extra space around code blocks.
\newcommand{\AgdaSpaceAroundCode}{%
\setboolean{Agda@SpaceAroundCode}{true}}
% By default space is inserted around code blocks.
\AgdaSpaceAroundCode{}
% Sometimes one might want to break up a code block into multiple
% pieces, but keep code in different blocks aligned with respect to
% each other. Then one can use the AgdaAlign environment. Example
% usage:
%
% \begin{AgdaAlign}
% \begin{code}
% code
% code (more code)
% \end{code}
% Explanation...
% \begin{code}
% aligned with "code"
% code (aligned with (more code))
% \end{code}
% \end{AgdaAlign}
%
% Note that AgdaAlign environments should not be nested.
%
% Sometimes one might also want to hide code in the middle of a code
% block. This can be accomplished in the following way:
%
% \begin{AgdaAlign}
% \begin{code}
% visible
% \end{code}
% \begin{code}[hide]
% hidden
% \end{code}
% \begin{code}
% visible
% \end{code}
% \end{AgdaAlign}
%
% However, the result may be ugly: extra space is perhaps inserted
% around the code blocks.
%
% The AgdaSuppressSpace environment ensures that extra space is only
% inserted before the first code block, and after the last one (but
% not if \AgdaNoSpaceAroundCode{} is used). Example usage:
%
% \begin{AgdaAlign}
% \begin{code}
% code
% more code
% \end{code}
% Explanation...
% \begin{AgdaSuppressSpace}
% \begin{code}
% aligned with "code"
% aligned with "more code"
% \end{code}
% \begin{code}[hide]
% hidden code
% \end{code}
% \begin{code}
% also aligned with "more code"
% \end{code}
% \end{AgdaSuppressSpace}
% \end{AgdaAlign}
%
% Note that AgdaSuppressSpace environments should not be nested.
%
% There is also a combined environment, AgdaMultiCode, that combines
% the effects of AgdaAlign and AgdaSuppressSpace.
% The number of the current/next code block (excluding hidden ones).
\newcounter{Agda@Current}
\setcounter{Agda@Current}{0}
% The number of the previous code block (excluding hidden ones), used
% locally in \Agda@SuppressEnd.
\newcounter{Agda@Previous}
% Is AgdaAlign active?
\newboolean{Agda@Align}
\setboolean{Agda@Align}{false}
% The number of the first code block (if any) in a given AgdaAlign
% environment.
\newcounter{Agda@AlignStart}
\newcommand{\Agda@AlignStart}{%
\ifthenelse{\boolean{Agda@Align}}{%
\PackageError{agda}{Nested AgdaAlign environments}{%
AgdaAlign and AgdaMultiCode environments must not be
nested.}}{%
\setboolean{Agda@Align}{true}%
\setcounter{Agda@AlignStart}{\value{Agda@Current}}}}
\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}
\newenvironment{AgdaAlign}{%
\Agda@AlignStart{}}{%
\Agda@AlignEnd{}%
\ignorespacesafterend}
% Is AgdaSuppressSpace active?
\newboolean{Agda@Suppress}
\setboolean{Agda@Suppress}{false}
% The number of the first code block (if any) in a given
% AgdaSuppressSpace environment.
\newcounter{Agda@SuppressStart}
% Does a "do not suppress space after" label exist for the current
% code block? (This boolean is used locally in the code environment's
% implementation.)
\newboolean{Agda@DoNotSuppressSpaceAfter}
\newcommand{\Agda@SuppressStart}{%
\ifthenelse{\boolean{Agda@Suppress}}{%
\PackageError{agda}{Nested AgdaSuppressSpace environments}{%
AgdaSuppressSpace and AgdaMultiCode environments must not be
nested.}}{%
\setboolean{Agda@Suppress}{true}%
\setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}
% Marks the given code block as one that space should not be
% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are
% both active).
\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%
% The use of labels is intended to ensure that LaTeX will provide a
% warning if the document needs to be recompiled.
\label{Agda@DoNotSuppressSpaceAfter@#1}}
\newcommand{\Agda@SuppressEnd}{%
\ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%
% Mark the previous code block in the .aux file.
\setcounter{Agda@Previous}{\theAgda@Current-1}%
\immediate\write\@auxout{%
\noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%
\setboolean{Agda@Suppress}{false}}
\newenvironment{AgdaSuppressSpace}{%
\Agda@SuppressStart{}}{%
\Agda@SuppressEnd{}%
\ignorespacesafterend}
\newenvironment{AgdaMultiCode}{%
\Agda@AlignStart{}%
\Agda@SuppressStart{}}{%
\Agda@SuppressEnd{}%
\Agda@AlignEnd{}%
\ignorespacesafterend}
% Vertical space used for empty lines. By default \abovedisplayskip.
\newlength{\AgdaEmptySkip}
\setlength{\AgdaEmptySkip}{\abovedisplayskip}
% Extra space to be inserted for empty lines (the difference between
% \AgdaEmptySkip and \baselineskip). Used internally.
\newlength{\AgdaEmptyExtraSkip}
% Counter used for code numbers.
\newcounter{AgdaCodeNumber}
% Formats a code number.
\newcommand{\AgdaFormatCodeNumber}[1]{(#1)}
% A boolean used to handle the option number.
\newboolean{Agda@Number}
\setboolean{Agda@Number}{false}
% A boolean used to handle the option inline*. (For some reason the
% approach used for hide and inline does not work for inline*.)
\newboolean{Agda@InlineStar}
\setboolean{Agda@InlineStar}{false}
% Keys used by the code environment.
\define@boolkey[Agda]{code}{hide}[true]{}
\define@boolkey[Agda]{code}{inline}[true]{}
\define@boolkey[Agda]{code}{inline*}[true]{%
\setboolean{Agda@InlineStar}{true}}
\define@key[Agda]{code}{number}[]{%
\ifthenelse{\boolean{Agda@Number}}{}{%
\setboolean{Agda@Number}{true}%
% Increase the counter if this has not already been done.
\refstepcounter{AgdaCodeNumber}}%
% If the label is non-empty, set it. Note that it is possible to
% give several labels for a single code listing.
\ifthenelse{\equal{#1}{}}{}{\label{#1}}}
% The code environment.
%
% Options:
%
% * hide: The code is hidden. Other options are ignored.
%
% * number: Give the code an equation number.
%
% * number=l: Give the code an equation number and the label l. It is
% possible to use this option several times with different labels.
%
% * inline/inline*: The code is inlined. In this case most of the
% discussion above does not apply, alignment is not respected, and so
% on. It is recommended to only use this option for a single line of
% code, and to not use two consecutive spaces in this piece of code.
%
% Note that this environment ignores spaces after its end. If a space
% (\AgdaSpace{}) should be inserted after the inline code, use
% inline*, otherwise use inline.
%
% When this option is used number is ignored.
%
% The implementation is based on plainhscode in lhs2TeX's
% polycode.fmt, written by Andres Löh.
\NewEnviron{code}[1][]{%
% Process the options. Complain about unknown options.
\setkeys[Agda]{code}[number]{#1}%
\ifAgda@code@hide%
% Hide the code.
\else%
\ifAgda@code@inline%
% Inline code.
%
% Make the polytable primitives emitted by the LaTeX backend
% do nothing.
\DeclareDocumentCommand{\>}{O{}O{}}{}%
\DeclareDocumentCommand{\<}{O{}}{}%
\AgdaCodeStyle\BODY%
\else%
\ifthenelse{\boolean{Agda@InlineStar}}{%
% Inline code with space at the end.
%
\DeclareDocumentCommand{\>}{O{}O{}}{}%
\DeclareDocumentCommand{\<}{O{}}{}%
\AgdaCodeStyle\BODY\AgdaSpace{}}{%
%
% Displayed code.
%
% Conditionally emit space before the code block. Unconditionally
% switch to a new line.
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
\(\not \boolean{Agda@Suppress} \or%
\value{Agda@SuppressStart} = \value{Agda@Current}\)}{%
\Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%
\Agda@NewlineWithVerticalSpace{0pt}}%
%
% Check if numbers have been requested. If they have, then a side
% effect of this call is that Agda@Number is set to true, the code
% number counter is increased, and the label (if any) is set.
\setkeys[Agda]{code}[hide,inline,inline*]{#1}%
\ifthenelse{\boolean{Agda@Number}}{%
% Equation numbers have been requested. Use a minipage, so that
% there is room for the code number to the right, and the code
% number becomes centered vertically.
\begin{minipage}{%
\linewidth-%
\widthof{%
\AgdaSpace{}%
\AgdaFormatCodeNumber{\theAgdaCodeNumber}}}}{}%
%
% Indent the entire code block.
\advance\leftskip\mathindent%
%
% The code's style can be customised.
\AgdaCodeStyle%
%
% Used to control the height of empty lines.
\setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%
%
% The environment used to handle indentation (of individual lines)
% and alignment.
\begin{pboxed}%
%
% Conditionally preserve alignment between code blocks.
\ifthenelse{\boolean{Agda@Align}}{%
\ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%
\savecolumns}{%
\restorecolumns}}{}%
%
% The code.
\BODY%
\end{pboxed}%
%
\ifthenelse{\boolean{Agda@Number}}{%
% Equation numbers have been requested.
\end{minipage}%
% Insert the code number to the right.
\hfill \AgdaFormatCodeNumber{\theAgdaCodeNumber}}{}%
%
% Does the label Agda@DoNotSuppressAfter@<current code block
% number> exist?
\ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%
\setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%
\setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%
%
% Conditionally emit space after the code block. Unconditionally
% switch to a new line.
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
\(\not \boolean{Agda@Suppress} \or%
\boolean{Agda@DoNotSuppressSpaceAfter}\)}{%
\Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%
\Agda@NewlineWithVerticalSpace{0pt}}%
%
% Step the code block counter, but only for non-hidden code.
\stepcounter{Agda@Current}}%
\fi%
\fi%
% Reset Agda@Number and Agda@InlineStar.
\setboolean{Agda@Number}{false}%
\setboolean{Agda@InlineStar}{false}}
% Space inserted after tokens.
\newcommand{\AgdaSpace}{ }
% Space inserted to indent something.
\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}
% Default column for polytable.
\defaultcolumn{@{}l@{\AgdaSpace{}}}
% \AgdaIndent expects a non-negative integer as its only argument.
% This integer should be the distance, in code blocks, to the thing
% relative to which the text is indented.
%
% The default implementation only indents if the thing that the text
% is indented relative to exists in the same code block or is wrapped
% in the same AgdaAlign or AgdaMultiCode environment.
\newcommand{\AgdaIndent}[1]{%
\ifthenelse{#1 = 0
\or
\( \boolean{Agda@Align}
\and
\cnttest{\value{Agda@Current} - #1}{>=}{
\value{Agda@AlignStart}}
\)}{\AgdaIndentSpace{}}{}}
% Underscores are typeset using \AgdaUnderscore{}.
\newcommand{\AgdaUnderscore}{\_}
\endinput