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
/
Issue2019.html

Issue2019.html 2.2 KB
Cronologia Originale

123456789101112131415161718192021222324252627 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>Issue2019</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. 

  5. \begin{document}
    6. 

  6. 

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

  8. <a id="75" class="Comment">-- We use non-standard spaces between the name of the term and the</a>
    9. 

  9. <a id="142" class="Comment">-- colon.</a>
    10. 

  10. <a id="152" class="Keyword">postulate</a>
    11. 

  11.   <a id="s00A0"></a><a id="164" href="Issue2019.html#164" class="Postulate">s00A0</a> <a id="170" class="Symbol">:</a> <a id="172" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="177" class="Comment">-- NO-BREAK SPACE        (&quot;\ &quot; with Agda input method)</a>
    12. 

  12.   <a id="s2004"></a><a id="234" href="Issue2019.html#234" class="Postulate">s2004</a> <a id="240" class="Symbol">:</a> <a id="242" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="247" class="Comment">-- THREE-PER-EM SPACE    (&quot;\;&quot; with Agda input method)</a>
    13. 

  13.   <a id="s202F"></a><a id="304" href="Issue2019.html#304" class="Postulate">s202F</a> <a id="310" class="Symbol">:</a> <a id="312" href="Agda.Primitive.html#311" class="Primitive">Set</a>  <a id="317" class="Comment">-- NARROW NO-BREAK SPACE (&quot;\,&quot; with Agda input method)</a>
    14. 

  14. <a id="372" class="Markup">\end{code}</a><a id="382" class="Background">
    15. 

  15. 

  16. % Various whitespace characters: &quot;    &quot;.
    17. 

  17. </a><a id="425" class="Markup">\begin{code}</a>
    18. 

  18. <a id="438" class="Keyword">open</a> <a id="443" class="Keyword">import</a> <a id="450" href="Agda.Builtin.String.html" class="Module">Agda.Builtin.String</a>
    19. 

  19. 

  20. <a id="471" class="Comment">-- Various whitespace characters: &quot;    &quot;.</a>
    21. 

  21. 

  22. <a id="various-whitespace-characters"></a><a id="514" href="Issue2019.html#514" class="Function">various-whitespace-characters</a> <a id="544" class="Symbol">:</a> <a id="546" href="Agda.Builtin.String.html#309" class="Postulate">String</a>
    23. 

  23. <a id="553" href="Issue2019.html#514" class="Function">various-whitespace-characters</a> <a id="583" class="Symbol">=</a> <a id="585" class="String">&quot;    &quot;</a>
    24. 

  24. <a id="592" class="Markup">\end{code}</a><a id="602" class="Background">
    25. 

  25. 

  26. \end{document}
    27. 

  27. </a></pre></body></html>
    28.