Home Esplora Aiuto
Accedi
caryoscelus
/
agda
Segui 1
Vota 0
Forka 0
File Problemi 0 Pull Requests 0 Wiki
Albero (Tree): ce9b406819
Rami (Branch) Tag
agda
/
test
/
LaTeXAndHTML
/
succeed
/
Tag.html

Tag.html 3.0 KB
Cronologia Originale

12345678910111213141516171819202122232425262728293031323334353637383940414243444546 
  1. <!DOCTYPE HTML>
    2. 

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

  3. 

  4. \usepackage[references]{agda}
    5. 

  5. 

  6. \begin{document}
    7. 

  7. 

  8. </a><a id="75" class="Markup">\begin{code}</a>
    9. 

  9. <a id="88" class="Keyword">module</a> <a id="95" href="Tag.html" class="Module">Tag</a> <a id="99" class="Keyword">where</a>
    10. 

  10. 

  11. <a id="106" class="Keyword">module</a> <a id="Apa"></a><a id="113" href="Tag.html#113" class="Module">Apa</a> <a id="117" class="Keyword">where</a>
    12. 

  12. 

  13. <a id="bepa"></a><a id="124" href="Tag.html#124" class="Function">bepa</a> <a id="129" class="Symbol">:</a> <a id="131" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="135" class="Symbol">→</a> <a id="137" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    14. 

  14. <a id="141" href="Tag.html#124" class="Function">bepa</a> <a id="146" href="Tag.html#146" class="Bound">x</a> <a id="148" class="Symbol">=</a> <a id="150" href="Tag.html#146" class="Bound">x</a>
    15. 

  15. 

  16. <a id="153" class="Keyword">data</a> <a id="Cepa"></a><a id="158" href="Tag.html#158" class="Datatype">Cepa</a> <a id="163" class="Symbol">:</a> <a id="165" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="169" class="Keyword">where</a>
    17. 

  17.   <a id="Cepa.cepa"></a><a id="177" href="Tag.html#177" class="InductiveConstructor">cepa</a> <a id="182" class="Symbol">:</a> <a id="184" href="Tag.html#158" class="Datatype">Cepa</a>
    18. 

  18. 

  19. <a id="190" class="Keyword">record</a> <a id="Depa"></a><a id="197" href="Tag.html#197" class="Record">Depa</a> <a id="202" class="Symbol">:</a> <a id="204" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="209" class="Keyword">where</a>
    20. 

  20.   <a id="217" class="Keyword">field</a>
    21. 

  21.     <a id="Depa.depa"></a><a id="227" href="Tag.html#227" class="Field">depa</a> <a id="232" class="Symbol">:</a> <a id="234" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    22. 

  22. 

  23. <a id="239" class="Keyword">postulate</a>
    24. 

  24.   <a id="epa"></a><a id="251" href="Tag.html#251" class="Postulate">epa</a> <a id="255" class="Symbol">:</a> <a id="257" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    25. 

  25. 

  26. <a id="262" class="Keyword">postulate</a>
    27. 

  27.   <a id="α"></a><a id="274" href="Tag.html#274" class="Postulate">α</a>   <a id="278" class="Symbol">:</a> <a id="280" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    28. 

  28.   <a id="_∘_"></a><a id="286" href="Tag.html#286" class="Postulate Operator">_∘_</a> <a id="290" class="Symbol">:</a> <a id="292" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    29. 

  29. <a id="296" class="Markup">\end{code}</a><a id="306" class="Background">
    30. 

  30. 

  31. \begin{tabular}{ll}
    32. 

  32.   Name &amp; Test \\
    33. 

  33.   \hline
    34. 

  34.   Apa   &amp; \AgdaRef{Apa} \\
    35. 

  35.   bepa  &amp; \AgdaRef{bepa} \\
    36. 

  36.   Cepa  &amp; \AgdaRef{Cepa} \\
    37. 

  37.   cepa  &amp; \AgdaRef{cepa} \\
    38. 

  38.   Depa  &amp; \AgdaRef{Depa} \\
    39. 

  39.   depa  &amp; \AgdaRef{depa} \\
    40. 

  40.   epa   &amp; \AgdaRef{epa} \\
    41. 

  41.   α     &amp; \AgdaRef{α} \\
    42. 

  42.   \_∘\_ &amp; \AgdaRef{\_∘\_} \\
    43. 

  43. \end{tabular}
    44. 

  44. 

  45. \end{document}
    46. 

  46. </a></pre></body></html>
    47.