+% ----------------------------------------------------------------------
+% Some useful commands when doing highlighting of Agda code in LaTeX.
+% ----------------------------------------------------------------------
+
+\ProvidesPackage{agda}
+
+\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox}
+
+% 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
+
+% XeLaTeX or LuaLaTeX
+\ifxetexorluatex
+
+ % Hack to get the amsthm package working.
+ % https://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete
+ \let\AgdaOpenBracket\[\let\AgdaCloseBracket\]
+ \RequirePackage{fontspec}
+ \let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
+ \RequirePackage{unicode-math}
+
+ \tracinglostchars=2 % If the font is missing some symbol, then say
+ % so in the compilation output.
+ \setmainfont
+ [ Ligatures = TeX
+ , BoldItalicFont = xits-bolditalic.otf
+ , BoldFont = xits-bold.otf
+ , ItalicFont = xits-italic.otf
+ ]
+ {xits-regular.otf}
+
+ \setmathfont{xits-math.otf}
+ \setmonofont[Mapping=tex-text]{FreeMono.otf}
+
+ % Make mathcal and mathscr appear as different.
+ % https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr
+ \setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{xits-math.otf}
+ \setmathfont[range=\mathscr]{xits-math.otf}
+
+ \providecommand{\DeclareUnicodeCharacter}[2]{\relax}
+
+% pdfLaTeX
+\else
+ \RequirePackage{ucs, amsfonts, amssymb}
+ \RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what
+ % safe does.
+
+ % https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
+ \RequirePackage[T1]{fontenc}
+ \RequirePackage[utf8x]{inputenc}
+\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
+
+% ----------------------------------------------------------------------
+% 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.
+
+\ifxetexorluatex
+ \newcommand{\AgdaFontStyle}[1]{\ensuremath{\mathsf{#1}}}
+ \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
+ \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
+ }{
+ \newcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathsf{#1}}}
+ }
+ \newcommand{\AgdaStringFontStyle}[1]{\ensuremath{\texttt{#1}}}
+ \newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\texttt{#1}}}
+ \newcommand{\AgdaBoundFontStyle}[1]{\ensuremath{\mathit{#1}}}
+
+\else
+ \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}}
+\fi
+
+% ----------------------------------------------------------------------
+% Colours.
+
+% ----------------------------------
+% The black and white colour scheme.
+\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
+
+ % Aspect colours.
+ \definecolor{AgdaComment} {HTML}{000000}
+ \definecolor{AgdaOption} {HTML}{000000}
+ \definecolor{AgdaKeyword} {HTML}{000000}
+ \definecolor{AgdaString} {HTML}{000000}
+ \definecolor{AgdaNumber} {HTML}{000000}
+ \definecolor{AgdaSymbol} {HTML}{000000}
+ \definecolor{AgdaPrimitiveType}{HTML}{000000}
+ \definecolor{AgdaOperator} {HTML}{000000}
+
+ % NameKind colours.
+ \definecolor{AgdaBound} {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{AgdaTerminationProblem}{HTML}{BEBEBE}
+ \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
+ \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{AgdaOption} {HTML}{000000}
+ \definecolor{AgdaKeyword} {HTML}{000000}
+ \definecolor{AgdaString} {HTML}{000000}
+ \definecolor{AgdaNumber} {HTML}{000000}
+ \definecolor{AgdaSymbol} {HTML}{000000}
+ \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
+ \definecolor{AgdaOperator} {HTML}{000000}
+
+ % NameKind colours.
+ \definecolor{AgdaBound} {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{AgdaTerminationProblem}{HTML}{FF0000}
+ \definecolor{AgdaIncompletePattern} {HTML}{A020F0}
+ \definecolor{AgdaError} {HTML}{F4A460}
+
+ % Misc.
+ \definecolor{AgdaHole} {HTML}{9DFF9D}
+
+% ----------------------------------
+% The standard colour scheme.
+}{
+ % Aspect colours.
+ \definecolor{AgdaComment} {HTML}{B22222}
+ \definecolor{AgdaOption} {HTML}{000000}
+ \definecolor{AgdaKeyword} {HTML}{CD6600}
+ \definecolor{AgdaString} {HTML}{B22222}
+ \definecolor{AgdaNumber} {HTML}{A020F0}
+ \definecolor{AgdaSymbol} {HTML}{404040}
+ \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
+ \definecolor{AgdaOperator} {HTML}{000000}
+
+ % NameKind colours.
+ \definecolor{AgdaBound} {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{AgdaTerminationProblem}{HTML}{FFA07A}
+ \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
+ \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{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}
+\newcommand{\AgdaOption} [1]
+ {\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaOption}{#1}}}}
+\newcommand{\AgdaKeyword} [1]
+ {\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}
+\newcommand{\AgdaString} [1]
+ {\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}
+\newcommand{\AgdaNumber} [1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}
+\newcommand{\AgdaSymbol} [1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}
+\newcommand{\AgdaPrimitiveType}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}
+\newcommand{\AgdaOperator} [1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaOperator}{#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{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}
+\newcommand{\AgdaInductiveConstructor}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaCoinductiveConstructor}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaDatatype}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaField}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaFunction}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaMacro}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaModule}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaPostulate}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaPrimitive}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}
+\newcommand{\AgdaRecord}[1]
+ {\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+\newcommand{\AgdaArgument}[1]
+ {\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\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{\AgdaTerminationProblem}[1]
+ {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
+\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
+\newcommand{\AgdaError} [1]
+ {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
+
+% Misc.
+\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
+\long\def\AgdaHide#1{\ignorespaces} % Used to hide code from LaTeX.
+
+% ----------------------------------------------------------------------
+% The code environment.
+
+\newcommand{\AgdaCodeStyle}{\fontsize{12pt}{14pt}}
+% \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{\AgdaNewlineWithVerticalSpace}[1]{%
+ {\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
+
+% 0: No space around code. 1: Space around code.
+\newcounter{Agda@SpaceAroundCode}
+
+% Use this command to avoid extra space around code blocks.
+\newcommand{\AgdaNoSpaceAroundCode}{%
+ \setcounter{Agda@SpaceAroundCode}{0}}
+
+% Use this command to include extra space around code blocks.
+\newcommand{\AgdaSpaceAroundCode}{%
+ \setcounter{Agda@SpaceAroundCode}{1}}
+
+% 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}
+% \AgdaHide{
+% \begin{code}
+% 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).
+%
+% The environment takes one argument, the number of wrapped code
+% blocks (excluding hidden ones). Example usage:
+%
+% \begin{AgdaAlign}
+% \begin{code}
+% code
+% more code
+% \end{code}
+% Explanation...
+% \begin{AgdaSuppressSpace}{2}
+% \begin{code}
+% aligned with "code"
+% aligned with "more code"
+% \end{code}
+% \AgdaHide{
+% \begin{code}
+% 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.
+
+% 0: AgdaAlign is not active. 1: AgdaAlign is active.
+\newcounter{Agda@Align}
+\setcounter{Agda@Align}{0}
+
+% The current code block.
+\newcounter{Agda@AlignCurrent}
+
+\newcommand{\Agda@AlignStart}{%
+ \setcounter{Agda@Align}{1}%
+ \setcounter{Agda@AlignCurrent}{1}}
+
+\newcommand{\Agda@AlignEnd}{\setcounter{Agda@Align}{0}}
+
+\newenvironment{AgdaAlign}{%
+ \Agda@AlignStart{}}{%
+ \Agda@AlignEnd{}%
+ \ignorespacesafterend}
+
+% 0: AgdaSuppressSpace is not active. 1: AgdaSuppressSpace is active.
+\newcounter{Agda@Suppress}
+\setcounter{Agda@Suppress}{0}
+
+% The current code block.
+\newcounter{Agda@SuppressCurrent}
+
+% The expected number of code blocks.
+\newcounter{Agda@SuppressLast}
+
+\newcommand{\Agda@SuppressStart}[1]{%
+ \setcounter{Agda@Suppress}{1}%
+ \setcounter{Agda@SuppressLast}{#1}%
+ \setcounter{Agda@SuppressCurrent}{1}}
+
+\newcommand{\Agda@SuppressEnd}{\setcounter{Agda@Suppress}{0}}
+
+\newenvironment{AgdaSuppressSpace}[1]{%
+ \Agda@SuppressStart{#1}}{%
+ \Agda@SuppressEnd{}%
+ \ignorespacesafterend}
+
+\newenvironment{AgdaMultiCode}[1]{%
+ \Agda@AlignStart{}%
+ \Agda@SuppressStart{#1}}{%
+ \Agda@SuppressEnd{}%
+ \Agda@AlignEnd{}%
+ \ignorespacesafterend}
+
+% The code environment.
+%
+% The implementation is based on plainhscode in lhs2TeX's
+% polycode.fmt, written by Andres Löh.
+\newenvironment{code}{%
+ \ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or%
+ \not \(\value{Agda@Suppress} = 0 \or%
+ \value{Agda@SuppressCurrent} = 1\)}{%
+ \AgdaNewlineWithVerticalSpace{0pt}}{%
+ \AgdaNewlineWithVerticalSpace{\abovedisplayskip}}%
+ \advance\leftskip\mathindent%
+ \AgdaCodeStyle%
+ \pboxed%
+ \ifthenelse{\value{Agda@Align} = 0}{}{%
+ \ifthenelse{\value{Agda@AlignCurrent} = 1}{%
+ \savecolumns}{%
+ \restorecolumns}}}{%
+ \endpboxed%
+ \ifthenelse{\value{Agda@SpaceAroundCode} = 0 \or%
+ \not \(\value{Agda@Suppress} = 0 \or%
+ \value{Agda@SuppressCurrent} =%
+ \value{Agda@SuppressLast}\)}{%
+ \AgdaNewlineWithVerticalSpace{0pt}}{%
+ \AgdaNewlineWithVerticalSpace{\belowdisplayskip}}%
+ \stepcounter{Agda@AlignCurrent}%
+ \stepcounter{Agda@SuppressCurrent}%
+ \ignorespacesafterend}
+
+% 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
+ \( \value{Agda@Align} = 1
+ \AND
+ #1 < \value{Agda@AlignCurrent}
+ \)}{\AgdaIndentSpace{}}{}}
+
+\endinput