Etusivu Tutki Apua
Kirjaudu sisään
caryoscelus
/
agda
Tarkkaile 1
Äänestä 0
Fork 0
Tiedostot Ongelmat 0 Pull-pyynnöt 0 Wiki
Puu: ce9b406819
Branchit Tagit
agda
/
test
/
LaTeXAndHTML
/
succeed
/
Less-extra-indentation.html

Less-extra-indentation.html 8.8 KB
Historia Raaka

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147 
  1. <!DOCTYPE HTML>
    2. 

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

  3. 

  4. \usepackage{agda}
    5. 

  5. 

  6. \usepackage{amsmath}
    7. 

  7. \usepackage{newunicodechar}
    8. 

  8. \newunicodechar{₁}{\ensuremath{{}_{\text{1}}}}
    9. 

  9. 

  10. \pagestyle{empty}
    11. 

  11. 

  12. \begin{document}
    13. 

  13. 

  14. \noindent Control:
    15. 

  15. </a><a id="198" class="Markup">\begin{code}</a>
    16. 

  16.   <a id="213" href="Less-extra-indentation.html#213" class="Function">_</a> <a id="215" class="Symbol">:</a> <a id="217" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    17. 

  17.   <a id="224" class="Symbol">_</a> <a id="226" class="Symbol">=</a> <a id="228" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    18. 

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

  19. 

  20. \noindent No extra indentation (alignment):
    21. 

  21. </a><a id="288" class="Markup">\begin{code}[hide]</a>
    22. 

  22.   <a id="309" href="Less-extra-indentation.html#309" class="Function">_</a> <a id="311" class="Symbol">:</a> <a id="313" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    23. 

  23.   <a id="320" class="Symbol">_</a> <a id="322" class="Symbol">=</a>
    24. 

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

  25. </a><a id="335" class="Markup">\begin{code}</a>
    26. 

  26.     <a id="352" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    27. 

  27. <a id="356" class="Markup">\end{code}</a><a id="366" class="Background">
    28. 

  28. 

  29. \noindent No extra indentation (indentation):
    30. 

  30. </a><a id="414" class="Markup">\begin{code}[hide]</a>
    31. 

  31.   <a id="435" href="Less-extra-indentation.html#435" class="Function">_</a> <a id="437" class="Symbol">:</a> <a id="439" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    32. 

  32.   <a id="446" class="Symbol">_</a> <a id="448" class="Symbol">=</a>
    33. 

  33. <a id="450" class="Markup">\end{code}</a><a id="460" class="Background">
    34. 

  34. </a><a id="461" class="Markup">\begin{code}</a>
    35. 

  35.      <a id="479" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    36. 

  36. <a id="483" class="Markup">\end{code}</a><a id="493" class="Background">
    37. 

  37. 

  38. \noindent No extra indentation (alignment):
    39. 

  39. </a><a id="539" class="Markup">\begin{code}[hide]</a>
    40. 

  40.   <a id="560" class="Keyword">postulate</a>
    41. 

  41.     <a id="574" href="Less-extra-indentation.html#574" class="Postulate">_</a> <a id="576" class="Symbol">:</a>
    42. 

  42. <a id="578" class="Markup">\end{code}</a><a id="588" class="Background">
    43. 

  43. </a><a id="589" class="Markup">\begin{code}</a>
    44. 

  44.       <a id="608" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    45. 

  45. <a id="612" class="Markup">\end{code}</a><a id="622" class="Background">
    46. 

  46. 

  47. \noindent No extra indentation (indentation):
    48. 

  48. </a><a id="670" class="Markup">\begin{code}[hide]</a>
    49. 

  49.   <a id="691" class="Keyword">postulate</a>
    50. 

  50.     <a id="705" href="Less-extra-indentation.html#705" class="Postulate">_</a> <a id="707" class="Symbol">:</a>
    51. 

  51. <a id="709" class="Markup">\end{code}</a><a id="719" class="Background">
    52. 

  52. </a><a id="720" class="Markup">\begin{code}</a>
    53. 

  53.        <a id="740" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    54. 

  54. <a id="744" class="Markup">\end{code}</a><a id="754" class="Background">
    55. 

  55. 

  56. \noindent No extra indentation (alignment, \texttt{AgdaMultiCode}):
    57. 

  57. \begin{AgdaMultiCode}
    58. 

  58. </a><a id="846" class="Markup">\begin{code}[hide]</a>
    59. 

  59.   <a id="867" href="Less-extra-indentation.html#867" class="Function">_</a> <a id="869" class="Symbol">:</a> <a id="871" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    60. 

  60.   <a id="878" class="Symbol">_</a> <a id="880" class="Symbol">=</a>
    61. 

  61. <a id="882" class="Markup">\end{code}</a><a id="892" class="Background">
    62. 

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

  63.     <a id="910" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    64. 

  64. <a id="914" class="Markup">\end{code}</a><a id="924" class="Background">
    65. 

  65. </a><a id="925" class="Markup">\begin{code}[hide]</a>
    66. 

  66.   <a id="946" href="Less-extra-indentation.html#946" class="Function">_</a> <a id="948" class="Symbol">:</a> <a id="950" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    67. 

  67.   <a id="957" class="Symbol">_</a> <a id="959" class="Symbol">=</a>
    68. 

  68. <a id="961" class="Markup">\end{code}</a><a id="971" class="Background">
    69. 

  69. </a><a id="972" class="Markup">\begin{code}</a>
    70. 

  70.     <a id="989" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    71. 

  71. <a id="993" class="Markup">\end{code}</a><a id="1003" class="Background">
    72. 

  72. \end{AgdaMultiCode}
    73. 

  73. 

  74. \noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
    75. 

  75. \begin{AgdaMultiCode}
    76. 

  76. </a><a id="1114" class="Markup">\begin{code}[hide]</a>
    77. 

  77.   <a id="1135" href="Less-extra-indentation.html#1135" class="Function">_</a> <a id="1137" class="Symbol">:</a> <a id="1139" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    78. 

  78.   <a id="1146" class="Symbol">_</a> <a id="1148" class="Symbol">=</a>
    79. 

  79. <a id="1150" class="Markup">\end{code}</a><a id="1160" class="Background">
    80. 

  80. </a><a id="1161" class="Markup">\begin{code}</a>
    81. 

  81.      <a id="1179" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    82. 

  82. <a id="1183" class="Markup">\end{code}</a><a id="1193" class="Background">
    83. 

  83. </a><a id="1194" class="Markup">\begin{code}[hide]</a>
    84. 

  84.   <a id="1215" href="Less-extra-indentation.html#1215" class="Function">_</a> <a id="1217" class="Symbol">:</a> <a id="1219" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
    85. 

  85.   <a id="1226" class="Symbol">_</a> <a id="1228" class="Symbol">=</a>
    86. 

  86. <a id="1230" class="Markup">\end{code}</a><a id="1240" class="Background">
    87. 

  87. </a><a id="1241" class="Markup">\begin{code}</a>
    88. 

  88.      <a id="1259" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    89. 

  89. <a id="1263" class="Markup">\end{code}</a><a id="1273" class="Background">
    90. 

  90. \end{AgdaMultiCode}
    91. 

  91. 

  92. \noindent No extra indentation (alignment, \texttt{AgdaMultiCode}):
    93. 

  93. \begin{AgdaMultiCode}
    94. 

  94. </a><a id="1385" class="Markup">\begin{code}[hide]</a>
    95. 

  95.   <a id="1406" class="Keyword">postulate</a>
    96. 

  96.     <a id="1420" href="Less-extra-indentation.html#1420" class="Postulate">_</a> <a id="1422" class="Symbol">:</a>
    97. 

  97. <a id="1424" class="Markup">\end{code}</a><a id="1434" class="Background">
    98. 

  98. </a><a id="1435" class="Markup">\begin{code}</a>
    99. 

  99.       <a id="1454" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    100. 

  100. <a id="1458" class="Markup">\end{code}</a><a id="1468" class="Background">
    101. 

  101. </a><a id="1469" class="Markup">\begin{code}[hide]</a>
    102. 

  102.   <a id="1490" class="Keyword">postulate</a>
    103. 

  103.     <a id="1504" href="Less-extra-indentation.html#1504" class="Postulate">_</a> <a id="1506" class="Symbol">:</a>
    104. 

  104. <a id="1508" class="Markup">\end{code}</a><a id="1518" class="Background">
    105. 

  105. </a><a id="1519" class="Markup">\begin{code}</a>
    106. 

  106.       <a id="1538" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    107. 

  107. <a id="1542" class="Markup">\end{code}</a><a id="1552" class="Background">
    108. 

  108. \end{AgdaMultiCode}
    109. 

  109. 

  110. \noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
    111. 

  111. \begin{AgdaMultiCode}
    112. 

  112. </a><a id="1663" class="Markup">\begin{code}[hide]</a>
    113. 

  113.   <a id="1684" class="Keyword">postulate</a>
    114. 

  114.     <a id="1698" href="Less-extra-indentation.html#1698" class="Postulate">_</a> <a id="1700" class="Symbol">:</a>
    115. 

  115. <a id="1702" class="Markup">\end{code}</a><a id="1712" class="Background">
    116. 

  116. </a><a id="1713" class="Markup">\begin{code}</a>
    117. 

  117.        <a id="1733" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    118. 

  118. <a id="1737" class="Markup">\end{code}</a><a id="1747" class="Background">
    119. 

  119. </a><a id="1748" class="Markup">\begin{code}[hide]</a>
    120. 

  120.   <a id="1769" class="Keyword">postulate</a>
    121. 

  121.     <a id="1783" href="Less-extra-indentation.html#1783" class="Postulate">_</a> <a id="1785" class="Symbol">:</a>
    122. 

  122. <a id="1787" class="Markup">\end{code}</a><a id="1797" class="Background">
    123. 

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

  124.        <a id="1818" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    125. 

  125. <a id="1822" class="Markup">\end{code}</a><a id="1832" class="Background">
    126. 

  126. \end{AgdaMultiCode}
    127. 

  127. 

  128. \noindent Extra indentation (indentation, \texttt{AgdaMultiCode}):
    129. 

  129. \begin{AgdaMultiCode}
    130. 

  130. </a><a id="1943" class="Markup">\begin{code}[hide]</a>
    131. 

  131.   <a id="1964" class="Keyword">postulate</a>
    132. 

  132.     <a id="Aaa"></a><a id="1978" href="Less-extra-indentation.html#1978" class="Postulate">Aaa</a> <a id="1982" class="Symbol">:</a>
    133. 

  133. <a id="1984" class="Markup">\end{code}</a><a id="1994" class="Background">
    134. 

  134. </a><a id="1995" class="Markup">\begin{code}</a>
    135. 

  135.       <a id="2014" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    136. 

  136. <a id="2018" class="Markup">\end{code}</a><a id="2028" class="Background">
    137. 

  137. </a><a id="2029" class="Markup">\begin{code}[hide]</a>
    138. 

  138.   <a id="2050" class="Keyword">postulate</a>
    139. 

  139.     <a id="Bbb"></a><a id="2064" href="Less-extra-indentation.html#2064" class="Postulate">Bbb</a> <a id="2068" class="Symbol">:</a>
    140. 

  140. <a id="2070" class="Markup">\end{code}</a><a id="2080" class="Background">
    141. 

  141. </a><a id="2081" class="Markup">\begin{code}</a>
    142. 

  142.       <a id="2100" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    143. 

  143. <a id="2104" class="Markup">\end{code}</a><a id="2114" class="Background">
    144. 

  144. \end{AgdaMultiCode}
    145. 

  145. 

  146. \end{document}
    147. 

  147. </a></pre></body></html>
    148.