| 1234567891011121314151617181920 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>PatternSynonyms2</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
- \usepackage{agda}
- \begin{document}
- </a><a id="61" class="Markup">\begin{code}</a>
- <a id="74" class="Keyword">data</a> <a id="Nat"></a><a id="79" href="PatternSynonyms2.html#79" class="Datatype">Nat</a> <a id="83" class="Symbol">:</a> <a id="85" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="89" class="Keyword">where</a>
- <a id="Nat.zero"></a><a id="97" href="PatternSynonyms2.html#97" class="InductiveConstructor">zero</a> <a id="102" class="Symbol">:</a> <a id="104" href="PatternSynonyms2.html#79" class="Datatype">Nat</a>
- <a id="Nat.suc"></a><a id="110" href="PatternSynonyms2.html#110" class="InductiveConstructor">suc</a> <a id="114" class="Symbol">:</a> <a id="116" href="PatternSynonyms2.html#79" class="Datatype">Nat</a> <a id="120" class="Symbol">→</a> <a id="122" href="PatternSynonyms2.html#79" class="Datatype">Nat</a>
- <a id="127" class="Keyword">module</a> <a id="134" href="PatternSynonyms2.html#134" class="Module">_</a> <a id="136" class="Keyword">where</a>
- <a id="145" class="Keyword">pattern</a> <a id="153" href="PatternSynonyms2.html#153" class="InductiveConstructor">two</a> <a id="159" class="Symbol">=</a> <a id="161" href="PatternSynonyms2.html#110" class="InductiveConstructor">suc</a> <a id="165" class="Symbol">(</a><a id="166" href="PatternSynonyms2.html#110" class="InductiveConstructor">suc</a> <a id="170" href="PatternSynonyms2.html#97" class="InductiveConstructor">zero</a><a id="174" class="Symbol">)</a>
- <a id="178" class="Keyword">pattern</a> <a id="186" href="PatternSynonyms2.html#186" class="InductiveConstructor">three</a> <a id="192" class="Symbol">=</a> <a id="194" href="PatternSynonyms2.html#110" class="InductiveConstructor">suc</a> <a id="198" href="PatternSynonyms2.html#153" class="InductiveConstructor">two</a>
- <a id="203" class="Keyword">data</a> <a id="Bot"></a><a id="208" href="PatternSynonyms2.html#208" class="Datatype">Bot</a> <a id="212" class="Symbol">:</a> <a id="214" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="218" class="Keyword">where</a>
- <a id="224" class="Markup">\end{code}</a><a id="234" class="Background">
- \end{document}
- </a></pre></body></html>
|
