- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>HighlightOccurrences</title><link rel="stylesheet" href="Agda.css"><script type="text/javascript" src="highlight-hover.js"></script></head><body><pre class="Agda"><a id="1" class="Keyword">data</a> <a id="Nat"></a><a id="6" href="HighlightOccurrences.html#6" class="Datatype">Nat</a> <a id="10" class="Symbol">:</a> <a id="12" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="16" class="Keyword">where</a>
- <a id="Nat.nohana"></a><a id="24" href="HighlightOccurrences.html#24" class="InductiveConstructor">nohana</a> <a id="31" class="Symbol">:</a> <a id="33" href="HighlightOccurrences.html#6" class="Datatype">Nat</a>
- <a id="Nat.kibou"></a><a id="39" href="HighlightOccurrences.html#39" class="InductiveConstructor">kibou</a> <a id="46" class="Symbol">:</a> <a id="48" href="HighlightOccurrences.html#6" class="Datatype">Nat</a> <a id="52" class="Symbol">-></a> <a id="55" href="HighlightOccurrences.html#6" class="Datatype">Nat</a>
- <a id="one"></a><a id="60" href="HighlightOccurrences.html#60" class="Function">one</a> <a id="64" class="Symbol">=</a> <a id="66" href="HighlightOccurrences.html#39" class="InductiveConstructor">kibou</a> <a id="72" href="HighlightOccurrences.html#24" class="InductiveConstructor">nohana</a>
- <a id="two"></a><a id="79" href="HighlightOccurrences.html#79" class="Function">two</a> <a id="83" class="Symbol">=</a> <a id="85" href="HighlightOccurrences.html#39" class="InductiveConstructor">kibou</a> <a id="91" href="HighlightOccurrences.html#60" class="Function">one</a>
- </pre></body></html>
|
