agda/test/LaTeXAndHTML/succeed/Issue3322.tex

% Nisse, 2018-10-26
% Testing that record field are already highlighted by scope checker.

\documentclass{article}

\usepackage{agda}

% This redefinition of AgdaField,
% in combination with the math-only command \bot,
% will fail the LaTeX build if no highlighting
% of fields has been performed.

\renewcommand{\AgdaField}[1]{\ensuremath{#1}}

\usepackage{amsmath}
\usepackage{newunicodechar}
\newunicodechar{₁}{\ensuremath{{}_{\text{1}}}}
\newunicodechar{₂}{\ensuremath{{}_{\text{2}}}}
\newunicodechar{⊥}{\bot}

\pagestyle{empty}

\begin{document}

\begin{code}%
\>[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{⊥}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set₁}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{r}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaRecord{R}\<%
\\
%
\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{r}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaKeyword{record}\AgdaSpace{}%
\AgdaSymbol{\{}\AgdaSpace{}%
\AgdaField{⊥}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\AgdaSpace{}%
\AgdaSymbol{\}}\<%
\end{code}

\end{document}