agda/test/LaTeXAndHTML/succeed/LaTeX-succeed.tex

\documentclass{article}

\usepackage{agda}

\begin{document}

\AgdaHide{
\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{LaTeX-succeed}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\end{code}
}

\begin{code}%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{true}%
\>[9]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[2]\AgdaInductiveConstructor{false}%
\>[9]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaOperator{\AgdaFunction{if\AgdaUnderscore{}then\AgdaUnderscore{}else\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaBound{A}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{if}}\AgdaSpace{}%
\AgdaInductiveConstructor{true}%
\>[10]\AgdaOperator{\AgdaFunction{then}}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{else}}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{t}\<%
\\
\>[0]\AgdaOperator{\AgdaFunction{if}}\AgdaSpace{}%
\AgdaInductiveConstructor{false}%
\>[10]\AgdaOperator{\AgdaFunction{then}}\AgdaSpace{}%
\AgdaBound{t}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{else}}\AgdaSpace{}%
\AgdaBound{f}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{f}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{zero}%
\>[8]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
%
\>[2]\AgdaInductiveConstructor{suc}%
\>[8]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
\>[0]\AgdaInductiveConstructor{zero}%
\>[17]\AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaBound{n}\<%
\\
\>[0]\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaBound{m}\AgdaSpace{}%
\AgdaComment{\{-\ ugh\ -\}}%
\>[17]\AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{m}\AgdaSpace{}%
\AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}%
\AgdaBound{n}\AgdaSymbol{)}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaSymbol{\{-\#}\AgdaSpace{}%
\AgdaKeyword{BUILTIN}\AgdaSpace{}%
\AgdaKeyword{NATURAL}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{\#-\}}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{alignment}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{m}\AgdaSpace{}%
\AgdaBound{n}\AgdaSpace{}%
\AgdaBound{o}\AgdaSpace{}%
\AgdaBound{p}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
\>[0]\AgdaFunction{alignment}%
\>[11]\AgdaNumber{0}%
\>[14]\AgdaNumber{1}%
\>[20]\AgdaNumber{2}%
\>[23]\AgdaNumber{3}%
\>[29]\AgdaSymbol{=}%
\>[32]\AgdaNumber{4}\<%
\\
\>[0]\AgdaFunction{alignment}%
\>[14]\AgdaNumber{1}%
\>[17]\AgdaNumber{2}%
\>[20]\AgdaNumber{3}%
\>[23]\AgdaNumber{4}%
\>[26]\AgdaSymbol{=}%
\>[29]\AgdaNumber{5}\<%
\\
\>[0]\AgdaFunction{alignment}%
\>[17]\AgdaNumber{2}%
\>[20]\AgdaNumber{3}%
\>[23]\AgdaNumber{4}%
\>[26]\AgdaNumber{5}%
\>[32]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaNumber{6}\<%
\\
\>[0]\AgdaCatchallClause{\AgdaFunction{alignment}}%
\>[20]\AgdaCatchallClause{\AgdaSymbol{\AgdaUnderscore{}}}%
\>[23]\AgdaCatchallClause{\AgdaSymbol{\AgdaUnderscore{}}}%
\>[26]\AgdaCatchallClause{\AgdaSymbol{\AgdaUnderscore{}}}%
\>[29]\AgdaCatchallClause{\AgdaSymbol{\AgdaUnderscore{}}}%
\>[32]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaNumber{0}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{⊥}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{record}\AgdaSpace{}%
\AgdaRecord{R}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{field}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaField{f}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\>[4]\AgdaField{g}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{record}\AgdaSpace{}%
\AgdaRecord{R′}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{field}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaField{h}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\>[4]\AgdaField{j}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\\
%
\>[4]\AgdaField{r}%
\>[7]\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{R}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{M}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaSymbol{∀}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSymbol{\}}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaRecord{R′}\AgdaSpace{}%
\AgdaBound{A}\AgdaSpace{}%
\AgdaBound{B}\<%
\\
%
\>[2]\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaKeyword{record}\<%
\\
\>[2][@{}l@{\AgdaIndent{0}}]%
\>[4]\AgdaSymbol{\{}\AgdaSpace{}%
\AgdaField{h}%
\>[9]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[4]\AgdaSymbol{;}\AgdaSpace{}%
\AgdaField{j}%
\>[9]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[4]\AgdaSymbol{;}\AgdaSpace{}%
\AgdaField{r}%
\>[112I]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaKeyword{record}\<%
\\
\>[.][@{}l@{}]\<[112I]%
\>[8]\AgdaSymbol{\{}\AgdaSpace{}%
\AgdaField{f}%
\>[13]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[8]\AgdaSymbol{;}\AgdaSpace{}%
\AgdaField{g}%
\>[13]\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[8]\AgdaSymbol{\}}\<%
\\
%
\>[4]\AgdaSymbol{\}}\<%
\end{code}

Andreas, 2018-04-03: The following two modules test the highlighting of projection patterns.

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{QualifiedProjectionPatterns}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaFunction{r}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{R}\<%
\\
%
\>[2]\AgdaFunction{r}\AgdaSpace{}%
\AgdaSymbol{.}\AgdaField{R.f}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[2]\AgdaFunction{r}\AgdaSpace{}%
\AgdaSymbol{.}\AgdaField{R.g}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{R′}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[2]\AgdaField{R′.h}\AgdaSpace{}%
\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[2]\AgdaField{R′.j}\AgdaSpace{}%
\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[2]\AgdaField{R′.r}\AgdaSpace{}%
\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{r}\<%
\end{code}

\begin{code}%
\>[0]\AgdaKeyword{module}\AgdaSpace{}%
\AgdaModule{UnqualifiedProjectionPatterns}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaKeyword{open}\AgdaSpace{}%
\AgdaModule{R}\AgdaSymbol{;}\AgdaSpace{}%
\AgdaKeyword{open}\AgdaSpace{}%
\AgdaModule{R′}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{r₀}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{R}\<%
\\
%
\>[2]\AgdaFunction{r₀}\AgdaSpace{}%
\AgdaSymbol{.}\AgdaField{f}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[2]\AgdaFunction{r₀}\AgdaSpace{}%
\AgdaSymbol{.}\AgdaField{g}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
%
\>[2]\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{R′}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[2]\AgdaField{h}\AgdaSpace{}%
\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{⊥}\<%
\\
%
\>[2]\AgdaField{j}\AgdaSpace{}%
\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaDatatype{Bool}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{Bool}\<%
\\
%
\>[2]\AgdaField{r}\AgdaSpace{}%
\AgdaFunction{r′}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{r₀}\<%
\end{code}

\end{document}