agda/test/LaTeXAndHTML/succeed/Issue3322.lagda

% 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}
record R : Set₂ where
  field
    ⊥ : Set₁

r : R

r = record { ⊥ = Set }
\end{code}

\end{document}