| 12345678910111213141516171819202122232425262728293031323334353637383940414243 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>MdDontHighlightCode</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">## MdDontHighlightCode
- </a><a id="25" class="Markup">```agda
- </a><a id="33" class="Keyword">module</a> <a id="40" href="MdDontHighlightCode.html" class="Module">MdDontHighlightCode</a> <a id="60" class="Keyword">where</a>
- <a id="66" class="Keyword">open</a> <a id="71" class="Keyword">import</a> <a id="78" href="Agda.Builtin.String.html" class="Module">Agda.Builtin.String</a>
- <a id="98" class="Markup">```
- </a><a id="102" class="Background">
- ### Marisa
- > Sure, but you're still just a tanuki, right?
- > The kind that drums on their bellies on the night of the full moon, right?
- </a><a id="240" class="Markup">```agda
- </a><a id="248" class="Keyword">module</a> <a id="TenDesires"></a><a id="255" href="MdDontHighlightCode.html#255" class="Module">TenDesires</a> <a id="266" class="Keyword">where</a>
- <a id="274" class="Keyword">record</a> <a id="TenDesires.Marisa"></a><a id="281" href="MdDontHighlightCode.html#281" class="Record">Marisa</a> <a id="288" class="Symbol">:</a> <a id="290" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="294" class="Keyword">where</a>
- <a id="304" class="Keyword">constructor</a> <a id="TenDesires.MkSasa"></a><a id="316" href="MdDontHighlightCode.html#316" class="InductiveConstructor">MkSasa</a>
- <a id="327" class="Keyword">field</a>
- <a id="333" class="Markup">```
- </a><a id="337" class="Background">
- ### Mamizou
- > You are making light of us, are you not? What do you call yourself?
- </a><a id="422" class="Markup">```agda
- </a> <a id="TenDesires.Marisa.name"></a><a id="436" href="MdDontHighlightCode.html#436" class="Field">name</a> <a id="441" class="Symbol">:</a> <a id="443" href="Agda.Builtin.String.html#309" class="Postulate">String</a>
- <a id="450" class="Markup">```
- </a><a id="454" class="Background">
- ### Marisa
- > I'm Reimu Hakurei!
- </a><a id="489" class="Markup">```agda
- </a><a id="497" class="Keyword">open</a> <a id="502" href="MdDontHighlightCode.html#255" class="Module">TenDesires</a>
- <a id="513" class="Keyword">open</a> <a id="518" href="MdDontHighlightCode.html#281" class="Module">Marisa</a>
- <a id="525" href="MdDontHighlightCode.html#525" class="Function">_</a> <a id="527" class="Symbol">=</a> <a id="529" href="MdDontHighlightCode.html#316" class="InductiveConstructor">MkSasa</a> <a id="536" class="String">"Reimu Hakurei"</a>
- <a id="552" class="Markup">```
- </a><a id="556" class="Background">
- ### Mamizou
- > Marisa Kirisame, is it? I'll be sure to remember that.
- > I intend to take my revenge, so you'd best watch your back on the night of the full moon.
- </a></pre></body></html>
|
