Kezdőlap Felfedezés Súgó
Bejelentkezés
caryoscelus
/
agda
Figyelés 1
Kedvenc 0
Másolás 0
Fájlok Problémák 0 Beolvasztási kérések 0 Wiki
Fa: ce9b406819
Branch-ok Tag-ek
agda
/
test
/
LaTeXAndHTML
/
succeed
/
PatternSynonyms.html

PatternSynonyms.html 3.0 KB
Előzmények Nyers

123456789101112131415161718192021 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>PatternSynonyms</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
    3. 

  3. \usepackage{agda}
    4. 

  4. \begin{document}
    5. 

  5. 

  6. </a><a id="61" class="Markup">\begin{code}</a>
    7. 

  7. <a id="74" class="Keyword">data</a> <a id="Nat"></a><a id="79" href="PatternSynonyms.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>
    8. 

  8.   <a id="Nat.zero"></a><a id="97" href="PatternSynonyms.html#97" class="InductiveConstructor">zero</a> <a id="102" class="Symbol">:</a> <a id="104" href="PatternSynonyms.html#79" class="Datatype">Nat</a>
    9. 

  9.   <a id="Nat.suc"></a><a id="110" href="PatternSynonyms.html#110" class="InductiveConstructor">suc</a> <a id="114" class="Symbol">:</a> <a id="116" href="PatternSynonyms.html#79" class="Datatype">Nat</a> <a id="120" class="Symbol">→</a> <a id="122" href="PatternSynonyms.html#79" class="Datatype">Nat</a>
    10. 

  10. 

  11. <a id="127" class="Keyword">module</a> <a id="PatternSyns"></a><a id="134" href="PatternSynonyms.html#134" class="Module">PatternSyns</a> <a id="146" class="Keyword">where</a>
    12. 

  12.   <a id="154" class="Keyword">pattern</a> <a id="PatternSyns.two"></a><a id="162" href="PatternSynonyms.html#162" class="InductiveConstructor">two</a>   <a id="168" class="Symbol">=</a> <a id="170" href="PatternSynonyms.html#110" class="InductiveConstructor">suc</a> <a id="174" class="Symbol">(</a><a id="175" href="PatternSynonyms.html#110" class="InductiveConstructor">suc</a> <a id="179" href="PatternSynonyms.html#97" class="InductiveConstructor">zero</a><a id="183" class="Symbol">)</a>
    13. 

  13.   <a id="187" class="Keyword">pattern</a> <a id="PatternSyns.three"></a><a id="195" href="PatternSynonyms.html#195" class="InductiveConstructor">three</a> <a id="201" class="Symbol">=</a> <a id="203" href="PatternSynonyms.html#110" class="InductiveConstructor">suc</a> <a id="207" href="PatternSynonyms.html#162" class="InductiveConstructor">two</a>
    14. 

  14. 

  15. <a id="212" class="Keyword">open</a> <a id="217" href="PatternSynonyms.html#134" class="Module">PatternSyns</a> <a id="229" class="Keyword">using</a> <a id="235" class="Symbol">(</a><a id="236" href="PatternSynonyms.html#162" class="InductiveConstructor">two</a><a id="239" class="Symbol">)</a> <a id="241" class="Keyword">renaming</a> <a id="250" class="Symbol">(</a><a id="251" href="PatternSynonyms.html#195" class="InductiveConstructor">three</a> <a id="257" class="Symbol">to</a> <a id="260" class="InductiveConstructor">three′</a><a id="266" class="Symbol">)</a>
    16. 

  16. 

  17. <a id="269" class="Keyword">data</a> <a id="Bot"></a><a id="274" href="PatternSynonyms.html#274" class="Datatype">Bot</a> <a id="278" class="Symbol">:</a> <a id="280" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="284" class="Keyword">where</a>
    18. 

  18. <a id="290" class="Markup">\end{code}</a><a id="300" class="Background">
    19. 

  19. 

  20. \end{document}
    21. 

  21. </a></pre></body></html>
    22.