| 12345678910111213141516171819202122232425262728293031323334353637 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Issue3322</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">% 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}
- </a><a id="553" class="Markup">\begin{code}</a>
- <a id="566" class="Keyword">record</a> <a id="R"></a><a id="573" href="Issue3322.html#573" class="Record">R</a> <a id="575" class="Symbol">:</a> <a id="577" href="Agda.Primitive.html#311" class="Primitive">Set₂</a> <a id="582" class="Keyword">where</a>
- <a id="590" class="Keyword">field</a>
- <a id="R.⊥"></a><a id="600" href="Issue3322.html#600" class="Field">⊥</a> <a id="602" class="Symbol">:</a> <a id="604" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
- <a id="r"></a><a id="610" href="Issue3322.html#610" class="Function">r</a> <a id="612" class="Symbol">:</a> <a id="614" href="Issue3322.html#573" class="Record">R</a>
- <a id="617" href="Issue3322.html#610" class="Function">r</a> <a id="619" class="Symbol">=</a> <a id="621" class="Keyword">record</a> <a id="628" class="Symbol">{</a> <a id="630" href="Issue3322.html#600" class="Field">⊥</a> <a id="632" class="Symbol">=</a> <a id="634" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="638" class="Symbol">}</a>
- <a id="640" class="Markup">\end{code}</a><a id="650" class="Background">
- \end{document}
- </a></pre></body></html>
|
