agda/test/LaTeXAndHTML/succeed/MdHighlightCode.html

# MdHighlightCode

+ Avdol
  + Yes!
  + I!
  + Am!
+ Jojo!

> Jojo! This is the last of my hamon! Take it from me!!

**Everything above should be preserved**

```haskell
module Kira where
data KillerQueue

-- this code should be preserved
```

<pre class="agda-code"><a id="253" class="Keyword">module</a> <a id="260" href="MdHighlightCode.html" class="Module">MdHighlightCode</a> <a id="276" class="Keyword">where</a>

<a id="283" class="Keyword">open</a> <a id="288" class="Keyword">import</a> <a id="295" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
</pre>
This is an Agda code block ↑

<pre class="agda-code"><a id="number"></a><a id="351" href="MdHighlightCode.html#351" class="Function">number</a> <a id="358" class="Symbol">:</a> <a id="360" href="Agda.Builtin.Nat.html#97" class="Datatype">Nat</a>
<a id="364" href="MdHighlightCode.html#351" class="Function">number</a> <a id="371" class="Symbol">=</a> <a id="373" href="Agda.Builtin.Nat.html#128" class="InductiveConstructor">suc</a> <a id="377" class="Symbol">(</a><a id="378" href="Agda.Builtin.Nat.html#128" class="InductiveConstructor">suc</a> <a id="382" href="Agda.Builtin.Nat.html#115" class="InductiveConstructor">zero</a><a id="386" class="Symbol">)</a>
</pre>
This is an Agda code block as well ↑