% ---------------------------------------------------------------------- % 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.2.2.20221106 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{}). 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@ 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