Domů Procházet Nápověda
Přihlásit se
caryoscelus
/
agda
Sledovat 1
Oblíbit 0
Rozštěpit 0
Soubory Úkoly 0 Pull Requesty 0 Wiki
Strom: ce9b406819
Větve Značky
agda
/
test
/
LaTeXAndHTML
/
succeed
/
LaTeX-succeed.html

LaTeX-succeed.html 16 KB
Historie Surový

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>LaTeX-succeed</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. \begin{document}
    7. 

  7. 

  8. \AgdaHide{
    9. 

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

  10. <a id="87" class="Keyword">module</a> <a id="94" href="LaTeX-succeed.html" class="Module">LaTeX-succeed</a> <a id="108" class="Keyword">where</a>
    11. 

  11. <a id="114" class="Markup">\end{code}</a><a id="124" class="Background">
    12. 

  12. }
    13. 

  13. 

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

  15. <a id="141" class="Keyword">data</a> <a id="Bool"></a><a id="146" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="151" class="Symbol">:</a> <a id="153" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="157" class="Keyword">where</a>
    16. 

  16.   <a id="Bool.true"></a><a id="165" href="LaTeX-succeed.html#165" class="InductiveConstructor">true</a>   <a id="172" class="Symbol">:</a> <a id="174" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
    17. 

  17.   <a id="Bool.false"></a><a id="181" href="LaTeX-succeed.html#181" class="InductiveConstructor">false</a>  <a id="188" class="Symbol">:</a> <a id="190" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
    18. 

  18. 

  19. <a id="if_then_else_"></a><a id="196" href="LaTeX-succeed.html#196" class="Function Operator">if_then_else_</a> <a id="210" class="Symbol">:</a> <a id="212" class="Symbol">{</a><a id="213" href="LaTeX-succeed.html#213" class="Bound">A</a> <a id="215" class="Symbol">:</a> <a id="217" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="220" class="Symbol">}</a> <a id="222" class="Symbol">→</a> <a id="224" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="229" class="Symbol">→</a> <a id="231" href="LaTeX-succeed.html#213" class="Bound">A</a> <a id="233" class="Symbol">→</a> <a id="235" href="LaTeX-succeed.html#213" class="Bound">A</a> <a id="237" class="Symbol">→</a> <a id="239" href="LaTeX-succeed.html#213" class="Bound">A</a>
    20. 

  20. <a id="241" href="LaTeX-succeed.html#196" class="Function Operator">if</a> <a id="244" href="LaTeX-succeed.html#165" class="InductiveConstructor">true</a>   <a id="251" href="LaTeX-succeed.html#196" class="Function Operator">then</a> <a id="256" href="LaTeX-succeed.html#256" class="Bound">t</a> <a id="258" href="LaTeX-succeed.html#196" class="Function Operator">else</a> <a id="263" href="LaTeX-succeed.html#263" class="Bound">f</a> <a id="265" class="Symbol">=</a> <a id="267" href="LaTeX-succeed.html#256" class="Bound">t</a>
    21. 

  21. <a id="269" href="LaTeX-succeed.html#196" class="Function Operator">if</a> <a id="272" href="LaTeX-succeed.html#181" class="InductiveConstructor">false</a>  <a id="279" href="LaTeX-succeed.html#196" class="Function Operator">then</a> <a id="284" href="LaTeX-succeed.html#284" class="Bound">t</a> <a id="286" href="LaTeX-succeed.html#196" class="Function Operator">else</a> <a id="291" href="LaTeX-succeed.html#291" class="Bound">f</a> <a id="293" class="Symbol">=</a> <a id="295" href="LaTeX-succeed.html#291" class="Bound">f</a>
    22. 

  22. 

  23. <a id="298" class="Keyword">data</a> <a id="ℕ"></a><a id="303" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="305" class="Symbol">:</a> <a id="307" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="311" class="Keyword">where</a>
    24. 

  24.   <a id="ℕ.zero"></a><a id="319" href="LaTeX-succeed.html#319" class="InductiveConstructor">zero</a>  <a id="325" class="Symbol">:</a> <a id="327" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
    25. 

  25.   <a id="ℕ.suc"></a><a id="331" href="LaTeX-succeed.html#331" class="InductiveConstructor">suc</a>   <a id="337" class="Symbol">:</a> <a id="339" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="341" class="Symbol">→</a> <a id="343" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
    26. 

  26. 

  27. <a id="_+_"></a><a id="346" href="LaTeX-succeed.html#346" class="Function Operator">_+_</a> <a id="350" class="Symbol">:</a> <a id="352" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="354" class="Symbol">→</a> <a id="356" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="358" class="Symbol">→</a> <a id="360" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
    28. 

  28. <a id="362" href="LaTeX-succeed.html#319" class="InductiveConstructor">zero</a>             <a id="379" href="LaTeX-succeed.html#346" class="Function Operator">+</a> <a id="381" href="LaTeX-succeed.html#381" class="Bound">n</a> <a id="383" class="Symbol">=</a> <a id="385" href="LaTeX-succeed.html#381" class="Bound">n</a>
    29. 

  29. <a id="387" href="LaTeX-succeed.html#331" class="InductiveConstructor">suc</a> <a id="391" href="LaTeX-succeed.html#391" class="Bound">m</a> <a id="393" class="Comment">{- ugh -}</a>  <a id="404" href="LaTeX-succeed.html#346" class="Function Operator">+</a> <a id="406" href="LaTeX-succeed.html#406" class="Bound">n</a> <a id="408" class="Symbol">=</a> <a id="410" href="LaTeX-succeed.html#331" class="InductiveConstructor">suc</a> <a id="414" class="Symbol">(</a><a id="415" href="LaTeX-succeed.html#391" class="Bound">m</a> <a id="417" href="LaTeX-succeed.html#346" class="Function Operator">+</a> <a id="419" href="LaTeX-succeed.html#406" class="Bound">n</a><a id="420" class="Symbol">)</a>
    30. 

  30. 

  31. <a id="423" class="Symbol">{-#</a> <a id="427" class="Keyword">BUILTIN</a> <a id="435" class="Keyword">NATURAL</a> <a id="443" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a> <a id="445" class="Symbol">#-}</a>
    32. 

  32. 

  33. <a id="alignment"></a><a id="450" href="LaTeX-succeed.html#450" class="Function">alignment</a> <a id="460" class="Symbol">:</a> <a id="462" class="Symbol">(</a><a id="463" href="LaTeX-succeed.html#463" class="Bound">m</a> <a id="465" href="LaTeX-succeed.html#465" class="Bound">n</a> <a id="467" href="LaTeX-succeed.html#467" class="Bound">o</a> <a id="469" href="LaTeX-succeed.html#469" class="Bound">p</a> <a id="471" class="Symbol">:</a> <a id="473" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a><a id="474" class="Symbol">)</a> <a id="476" class="Symbol">→</a> <a id="478" href="LaTeX-succeed.html#303" class="Datatype">ℕ</a>
    34. 

  34. <a id="480" href="LaTeX-succeed.html#450" class="Function">alignment</a>  <a id="491" class="Number">0</a>  <a id="494" class="Number">1</a>     <a id="500" class="Number">2</a>  <a id="503" class="Number">3</a>     <a id="509" class="Symbol">=</a>  <a id="512" class="Number">4</a>
    35. 

  35. <a id="514" href="LaTeX-succeed.html#450" class="Function">alignment</a>     <a id="528" class="Number">1</a>  <a id="531" class="Number">2</a>  <a id="534" class="Number">3</a>  <a id="537" class="Number">4</a>  <a id="540" class="Symbol">=</a>  <a id="543" class="Number">5</a>
    36. 

  36. <a id="545" href="LaTeX-succeed.html#450" class="Function">alignment</a>        <a id="562" class="Number">2</a>  <a id="565" class="Number">3</a>  <a id="568" class="Number">4</a>  <a id="571" class="Number">5</a>     <a id="577" class="Symbol">=</a> <a id="579" class="Number">6</a>
    37. 

  37. <a id="581" href="LaTeX-succeed.html#450" class="CatchallClause Function">alignment</a><a id="590" class="CatchallClause">           </a><a id="601" class="CatchallClause Symbol">_</a><a id="602" class="CatchallClause">  </a><a id="604" class="CatchallClause Symbol">_</a><a id="605" class="CatchallClause">  </a><a id="607" class="CatchallClause Symbol">_</a><a id="608" class="CatchallClause">  </a><a id="610" class="CatchallClause Symbol">_</a>  <a id="613" class="Symbol">=</a> <a id="615" class="Number">0</a>
    38. 

  38. <a id="617" class="Markup">\end{code}</a><a id="627" class="Background">
    39. 

  39. 

  40. </a><a id="629" class="Markup">\begin{code}</a>
    41. 

  41. <a id="642" class="Keyword">data</a> <a id="⊥"></a><a id="647" href="LaTeX-succeed.html#647" class="Datatype">⊥</a> <a id="649" class="Symbol">:</a> <a id="651" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="655" class="Keyword">where</a>
    42. 

  42. 

  43. <a id="662" class="Keyword">record</a> <a id="R"></a><a id="669" href="LaTeX-succeed.html#669" class="Record">R</a> <a id="671" class="Symbol">:</a> <a id="673" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="678" class="Keyword">where</a>
    44. 

  44.   <a id="686" class="Keyword">field</a>
    45. 

  45.     <a id="R.f"></a><a id="696" href="LaTeX-succeed.html#696" class="Field">f</a>  <a id="699" class="Symbol">:</a> <a id="701" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    46. 

  46.     <a id="R.g"></a><a id="709" href="LaTeX-succeed.html#709" class="Field">g</a>  <a id="712" class="Symbol">:</a> <a id="714" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    47. 

  47. 

  48. <a id="719" class="Keyword">record</a> <a id="R′"></a><a id="726" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="729" class="Symbol">(</a><a id="730" href="LaTeX-succeed.html#730" class="Bound">A</a> <a id="732" href="LaTeX-succeed.html#732" class="Bound">B</a> <a id="734" class="Symbol">:</a> <a id="736" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="739" class="Symbol">)</a> <a id="741" class="Symbol">:</a> <a id="743" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="748" class="Keyword">where</a>
    49. 

  49.   <a id="756" class="Keyword">field</a>
    50. 

  50.     <a id="R′.h"></a><a id="766" href="LaTeX-succeed.html#766" class="Field">h</a>  <a id="769" class="Symbol">:</a> <a id="771" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    51. 

  51.     <a id="R′.j"></a><a id="779" href="LaTeX-succeed.html#779" class="Field">j</a>  <a id="782" class="Symbol">:</a> <a id="784" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    52. 

  52.     <a id="R′.r"></a><a id="792" href="LaTeX-succeed.html#792" class="Field">r</a>  <a id="795" class="Symbol">:</a> <a id="797" href="LaTeX-succeed.html#669" class="Record">R</a>
    53. 

  53. <a id="799" class="Markup">\end{code}</a><a id="809" class="Background">
    54. 

  54. 

  55. </a><a id="811" class="Markup">\begin{code}</a>
    56. 

  56. <a id="824" class="Keyword">module</a> <a id="M"></a><a id="831" href="LaTeX-succeed.html#831" class="Module">M</a> <a id="833" class="Keyword">where</a>
    57. 

  57.   <a id="M.r′"></a><a id="841" href="LaTeX-succeed.html#841" class="Function">r′</a> <a id="844" class="Symbol">:</a> <a id="846" class="Symbol">∀</a> <a id="848" class="Symbol">{</a><a id="849" href="LaTeX-succeed.html#849" class="Bound">A</a> <a id="851" href="LaTeX-succeed.html#851" class="Bound">B</a> <a id="853" class="Symbol">:</a> <a id="855" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="858" class="Symbol">}</a> <a id="860" class="Symbol">→</a> <a id="862" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="865" href="LaTeX-succeed.html#849" class="Bound">A</a> <a id="867" href="LaTeX-succeed.html#851" class="Bound">B</a>
    58. 

  58.   <a id="871" href="LaTeX-succeed.html#841" class="Function">r′</a> <a id="874" class="Symbol">=</a> <a id="876" class="Keyword">record</a>
    59. 

  59.     <a id="887" class="Symbol">{</a> <a id="889" href="LaTeX-succeed.html#766" class="Field">h</a>  <a id="892" class="Symbol">=</a> <a id="894" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    60. 

  60.     <a id="900" class="Symbol">;</a> <a id="902" href="LaTeX-succeed.html#779" class="Field">j</a>  <a id="905" class="Symbol">=</a> <a id="907" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    61. 

  61.     <a id="913" class="Symbol">;</a> <a id="915" href="LaTeX-succeed.html#792" class="Field">r</a> <a id="917" class="Symbol">=</a> <a id="919" class="Keyword">record</a>
    62. 

  62.         <a id="934" class="Symbol">{</a> <a id="936" href="LaTeX-succeed.html#696" class="Field">f</a>  <a id="939" class="Symbol">=</a> <a id="941" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    63. 

  63.         <a id="951" class="Symbol">;</a> <a id="953" href="LaTeX-succeed.html#709" class="Field">g</a>  <a id="956" class="Symbol">=</a> <a id="958" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    64. 

  64.         <a id="968" class="Symbol">}</a>
    65. 

  65.     <a id="974" class="Symbol">}</a>
    66. 

  66. <a id="976" class="Markup">\end{code}</a><a id="986" class="Background">
    67. 

  67. 

  68. Andreas, 2018-04-03: The following two modules test the highlighting of projection patterns.
    69. 

  69. 

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

  71. <a id="1095" class="Keyword">module</a> <a id="QualifiedProjectionPatterns"></a><a id="1102" href="LaTeX-succeed.html#1102" class="Module">QualifiedProjectionPatterns</a> <a id="1130" class="Keyword">where</a>
    72. 

  72. 

  73.   <a id="QualifiedProjectionPatterns.r"></a><a id="1139" href="LaTeX-succeed.html#1139" class="Function">r</a> <a id="1141" class="Symbol">:</a> <a id="1143" href="LaTeX-succeed.html#669" class="Record">R</a>
    74. 

  74.   <a id="1147" href="LaTeX-succeed.html#1139" class="Function">r</a> <a id="1149" class="Symbol">.</a><a id="1150" href="LaTeX-succeed.html#696" class="Field">R.f</a> <a id="1154" class="Symbol">=</a> <a id="1156" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
    75. 

  75.   <a id="1163" href="LaTeX-succeed.html#1139" class="Function">r</a> <a id="1165" class="Symbol">.</a><a id="1166" href="LaTeX-succeed.html#709" class="Field">R.g</a> <a id="1170" class="Symbol">=</a> <a id="1172" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    76. 

  76. 

  77.   <a id="QualifiedProjectionPatterns.r′"></a><a id="1177" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1180" class="Symbol">:</a> <a id="1182" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="1185" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1190" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    78. 

  78.   <a id="1194" href="LaTeX-succeed.html#766" class="Field">R′.h</a> <a id="1199" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1202" class="Symbol">=</a> <a id="1204" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    79. 

  79.   <a id="1208" href="LaTeX-succeed.html#779" class="Field">R′.j</a> <a id="1213" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1216" class="Symbol">=</a> <a id="1218" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1223" class="Symbol">→</a> <a id="1225" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
    80. 

  80.   <a id="1232" href="LaTeX-succeed.html#792" class="Field">R′.r</a> <a id="1237" href="LaTeX-succeed.html#1177" class="Function">r′</a> <a id="1240" class="Symbol">=</a> <a id="1242" href="LaTeX-succeed.html#1139" class="Function">r</a>
    81. 

  81. <a id="1244" class="Markup">\end{code}</a><a id="1254" class="Background">
    82. 

  82. 

  83. </a><a id="1256" class="Markup">\begin{code}</a>
    84. 

  84. <a id="1269" class="Keyword">module</a> <a id="UnqualifiedProjectionPatterns"></a><a id="1276" href="LaTeX-succeed.html#1276" class="Module">UnqualifiedProjectionPatterns</a> <a id="1306" class="Keyword">where</a>
    85. 

  85.   <a id="1314" class="Keyword">open</a> <a id="1319" href="LaTeX-succeed.html#669" class="Module">R</a><a id="1320" class="Symbol">;</a> <a id="1322" class="Keyword">open</a> <a id="1327" href="LaTeX-succeed.html#726" class="Module">R′</a>
    86. 

  86. 

  87.   <a id="UnqualifiedProjectionPatterns.r₀"></a><a id="1333" href="LaTeX-succeed.html#1333" class="Function">r₀</a> <a id="1336" class="Symbol">:</a> <a id="1338" href="LaTeX-succeed.html#669" class="Record">R</a>
    88. 

  88.   <a id="1342" href="LaTeX-succeed.html#1333" class="Function">r₀</a> <a id="1345" class="Symbol">.</a><a id="1346" href="LaTeX-succeed.html#696" class="Field">f</a> <a id="1348" class="Symbol">=</a> <a id="1350" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
    89. 

  89.   <a id="1357" href="LaTeX-succeed.html#1333" class="Function">r₀</a> <a id="1360" class="Symbol">.</a><a id="1361" href="LaTeX-succeed.html#709" class="Field">g</a> <a id="1363" class="Symbol">=</a> <a id="1365" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    90. 

  90. 

  91.   <a id="UnqualifiedProjectionPatterns.r′"></a><a id="1370" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1373" class="Symbol">:</a> <a id="1375" href="LaTeX-succeed.html#726" class="Record">R′</a> <a id="1378" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1383" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    92. 

  92.   <a id="1387" href="LaTeX-succeed.html#766" class="Field">h</a> <a id="1389" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1392" class="Symbol">=</a> <a id="1394" href="LaTeX-succeed.html#647" class="Datatype">⊥</a>
    93. 

  93.   <a id="1398" href="LaTeX-succeed.html#779" class="Field">j</a> <a id="1400" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1403" class="Symbol">=</a> <a id="1405" href="LaTeX-succeed.html#146" class="Datatype">Bool</a> <a id="1410" class="Symbol">→</a> <a id="1412" href="LaTeX-succeed.html#146" class="Datatype">Bool</a>
    94. 

  94.   <a id="1419" href="LaTeX-succeed.html#792" class="Field">r</a> <a id="1421" href="LaTeX-succeed.html#1370" class="Function">r′</a> <a id="1424" class="Symbol">=</a> <a id="1426" href="LaTeX-succeed.html#1333" class="Function">r₀</a>
    95. 

  95. <a id="1429" class="Markup">\end{code}</a><a id="1439" class="Background">
    96. 

  96. 

  97. \end{document}
    98. 

  98. </a></pre></body></html>
    99.