agda/test/LaTeXAndHTML/succeed/OrgHighlightCode.org

Org mode

• A list item!
• Another1

<p>
<pre class="Agda">
</p>
<p>
<a id="58" class="Keyword">module</a> <a id="65" href="OrgHighlightCode.html" class="Module">OrgHighlightCode</a> <a id="82" class="Keyword">where</a>
</p>

<p>
<a id="89" class="Keyword">data</a> <a id="Bool"></a><a id="94" href="OrgHighlightCode.html#94" class="Datatype">Bool</a> <a id="99" class="Symbol">:</a> <a id="101" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="105" class="Keyword">where</a>
</p>
<p>
</pre>
</p>

Some prose. Some more code.

<p>
<pre class="Agda">
</p>
<p>
  <a id="Bool.true"></a><a id="171" href="OrgHighlightCode.html#171" class="InductiveConstructor">true</a>  <a id="177" class="Symbol">:</a> <a id="179" href="OrgHighlightCode.html#94" class="Datatype">Bool</a>
</p>
<p>
  <a id="Bool.false"></a><a id="186" href="OrgHighlightCode.html#186" class="InductiveConstructor">false</a> <a id="192" class="Symbol">:</a> <a id="194" href="OrgHighlightCode.html#94" class="Datatype">Bool</a>
</p>
<p>
</pre>
</p>