Home Verkennen Help
Inloggen
caryoscelus
/
agda
Volgen 1
Ster 0
Vork 0
Bestanden Kwesties 0 Pull-aanvragen 0 Wiki
Boom: ce9b406819
Aftakkingen Labels
agda
/
test
/
LaTeXAndHTML
/
succeed
/
Links.html

Links.html 5.0 KB
Geschiedenis Ruwe

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758 
  1. <!DOCTYPE HTML>
    2. 

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

  3. \usepackage{hyperref}
    4. 

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

  5. \begin{document}
    6. 

  6. 

  7. \AgdaTarget{ℕ}
    8. 

  8. \AgdaTarget{zero}
    9. 

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

  10. <a id="136" class="Keyword">data</a> <a id="ℕ"></a><a id="141" href="Links.html#141" class="Datatype">ℕ</a> <a id="143" class="Symbol">:</a> <a id="145" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="149" class="Keyword">where</a>
    11. 

  11.   <a id="ℕ.zero"></a><a id="157" href="Links.html#157" class="InductiveConstructor">zero</a>  <a id="163" class="Symbol">:</a> <a id="165" href="Links.html#141" class="Datatype">ℕ</a>
    12. 

  12.   <a id="ℕ.suc"></a><a id="169" href="Links.html#169" class="InductiveConstructor">suc</a>   <a id="175" class="Symbol">:</a> <a id="177" href="Links.html#141" class="Datatype">ℕ</a> <a id="179" class="Symbol">→</a> <a id="181" href="Links.html#141" class="Datatype">ℕ</a>
    13. 

  13. <a id="183" class="Markup">\end{code}</a><a id="193" class="Background">
    14. 

  14. 

  15. See next page for how to define \AgdaFunction{two} (doesn&#39;t turn into a
    16. 

  16. link because the target hasn&#39;t been defined yet). We could do it
    17. 

  17. manually though; \hyperlink{two}{\AgdaDatatype{two}}.
    18. 

  18. 

  19. \newpage
    20. 

  20. 

  21. \AgdaTarget{two}
    22. 

  22. \hypertarget{two}{}
    23. 

  23. </a><a id="434" class="Markup">\begin{code}</a>
    24. 

  24. <a id="two"></a><a id="447" href="Links.html#447" class="Function">two</a> <a id="451" class="Symbol">:</a> <a id="453" href="Links.html#141" class="Datatype">ℕ</a>
    25. 

  25. <a id="455" href="Links.html#447" class="Function">two</a> <a id="459" class="Symbol">=</a> <a id="461" href="Links.html#169" class="InductiveConstructor">suc</a> <a id="465" class="Symbol">(</a><a id="466" href="Links.html#169" class="InductiveConstructor">suc</a> <a id="470" href="Links.html#157" class="InductiveConstructor">zero</a><a id="474" class="Symbol">)</a>
    26. 

  26. <a id="476" class="Markup">\end{code}</a><a id="486" class="Background">
    27. 

  27. 

  28. \AgdaInductiveConstructor{zero} is of type
    29. 

  29. \AgdaDatatype{ℕ}. \AgdaInductiveConstructor{suc} has not been defined to
    30. 

  30. be a target so it doesn&#39;t turn into a link.
    31. 

  31. 

  32. \newpage
    33. 

  33. 

  34. Now that the target for \AgdaFunction{two} has been defined the link
    35. 

  35. works automatically.
    36. 

  36. 

  37. </a><a id="750" class="Markup">\begin{code}</a>
    38. 

  38. <a id="763" class="Keyword">data</a> <a id="Bool"></a><a id="768" href="Links.html#768" class="Datatype">Bool</a> <a id="773" class="Symbol">:</a> <a id="775" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="779" class="Keyword">where</a>
    39. 

  39.   <a id="Bool.true"></a><a id="787" href="Links.html#787" class="InductiveConstructor">true</a> <a id="Bool.false"></a><a id="792" href="Links.html#792" class="InductiveConstructor">false</a> <a id="798" class="Symbol">:</a> <a id="800" href="Links.html#768" class="Datatype">Bool</a>
    40. 

  40. <a id="805" class="Markup">\end{code}</a><a id="815" class="Background">
    41. 

  41. 

  42. The AgdaTarget command takes a list as input, enabling several targets
    43. 

  43. to be specified as follows:
    44. 

  44. 

  45. \AgdaTarget{if, then, else, if\_then\_else\_}
    46. 

  46. </a><a id="963" class="Markup">\begin{code}</a>
    47. 

  47. <a id="if_then_else_"></a><a id="976" href="Links.html#976" class="Function Operator">if_then_else_</a> <a id="990" class="Symbol">:</a> <a id="992" class="Symbol">{</a><a id="993" href="Links.html#993" class="Bound">A</a> <a id="995" class="Symbol">:</a> <a id="997" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="1000" class="Symbol">}</a> <a id="1002" class="Symbol">→</a> <a id="1004" href="Links.html#768" class="Datatype">Bool</a> <a id="1009" class="Symbol">→</a> <a id="1011" href="Links.html#993" class="Bound">A</a> <a id="1013" class="Symbol">→</a> <a id="1015" href="Links.html#993" class="Bound">A</a> <a id="1017" class="Symbol">→</a> <a id="1019" href="Links.html#993" class="Bound">A</a>
    48. 

  48. <a id="1021" href="Links.html#976" class="Function Operator">if</a> <a id="1024" href="Links.html#787" class="InductiveConstructor">true</a> <a id="1029" href="Links.html#976" class="Function Operator">then</a> <a id="1034" href="Links.html#1034" class="Bound">t</a> <a id="1036" href="Links.html#976" class="Function Operator">else</a> <a id="1041" href="Links.html#1041" class="Bound">f</a> <a id="1043" class="Symbol">=</a> <a id="1045" href="Links.html#1034" class="Bound">t</a>
    49. 

  49. <a id="1047" href="Links.html#976" class="Function Operator">if</a> <a id="1050" href="Links.html#792" class="InductiveConstructor">false</a> <a id="1056" href="Links.html#976" class="Function Operator">then</a> <a id="1061" href="Links.html#1061" class="Bound">t</a> <a id="1063" href="Links.html#976" class="Function Operator">else</a> <a id="1068" href="Links.html#1068" class="Bound">f</a> <a id="1070" class="Symbol">=</a> <a id="1072" href="Links.html#1068" class="Bound">f</a>
    50. 

  50. <a id="1074" class="Markup">\end{code}</a><a id="1084" class="Background">
    51. 

  51. 

  52. \newpage
    53. 

  53. 

  54. Mixfix identifier need their underscores escaped:
    55. 

  55. \AgdaFunction{if\_then\_else\_}.
    56. 

  56. 

  57. \end{document}
    58. 

  58. </a></pre></body></html>
    59.