This is a literate Agda file.

Here's some inline code:

- This is a link to the record below: `Record`{.agda}
- This is not: `Record`
- This is a link with alternate text: `also a link`{.agda ident=Record}

<pre class="Agda"><a id="217" class="Keyword">record</a> <a id="Record"></a><a id="224" href="example.html#224" class="Record">Record</a> <a id="231" class="Symbol">:</a> <a id="233" class="PrimitiveType">Set</a> <a id="237" class="Keyword">where</a>
  <a id="245" class="Keyword">constructor</a> <a id="hey-look"></a><a id="257" href="example.html#257" class="InductiveConstructor">hey-look</a>
</pre>