Главная Обзор Помощь
Вход
caryoscelus
/
agda
Следить 1
В избранное 0
Ответвить 0
Файлы Обсуждения 0 Запросы на слияние 0 Вики
Дерево: ce9b406819
Ветки Метки
agda
/
test
/
LaTeXAndHTML
/
succeed
/
Issue1062.html

Issue1062.html 18 KB
История Исходник

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273 
  1. <!DOCTYPE HTML>
    2. 

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

  3. \documentclass{article}
    4. 

  4. 

  5. \usepackage{agda}
    6. 

  6. 

  7. \begin{document}
    8. 

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

  9. 

  10. <a id="89" class="Symbol">{-#</a> <a id="93" class="Keyword">OPTIONS</a> <a id="101" class="Pragma">--copatterns</a> <a id="114" class="Pragma">--sized-types</a> <a id="128" class="Symbol">#-}</a>
    11. 

  11. 

  12. <a id="133" class="Symbol">{-#</a> <a id="137" class="Keyword">BUILTIN</a> <a id="145" class="Keyword">SIZE</a>    <a id="Size"></a><a id="153" href="Issue1062.html#153" class="Postulate">Size</a>   <a id="160" class="Symbol">#-}</a>
    13. 

  13. <a id="164" class="Symbol">{-#</a> <a id="168" class="Keyword">BUILTIN</a> <a id="176" class="Keyword">SIZELT</a>  <a id="Size&lt;_"></a><a id="184" href="Issue1062.html#184" class="Postulate Operator">Size&lt;_</a> <a id="191" class="Symbol">#-}</a>
    14. 

  14. <a id="195" class="Symbol">{-#</a> <a id="199" class="Keyword">BUILTIN</a> <a id="207" class="Keyword">SIZESUC</a> <a id="↑_"></a><a id="215" href="Issue1062.html#215" class="Postulate Operator">↑_</a>     <a id="222" class="Symbol">#-}</a>
    15. 

  15. <a id="226" class="Symbol">{-#</a> <a id="230" class="Keyword">BUILTIN</a> <a id="238" class="Keyword">SIZEINF</a> <a id="∞"></a><a id="246" href="Issue1062.html#246" class="Postulate">∞</a>      <a id="253" class="Symbol">#-}</a>
    16. 

  16. 

  17. <a id="258" class="Keyword">data</a> <a id="List"></a><a id="263" href="Issue1062.html#263" class="Datatype">List</a> <a id="268" class="Symbol">(</a><a id="269" href="Issue1062.html#269" class="Bound">A</a> <a id="271" class="Symbol">:</a> <a id="273" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="276" class="Symbol">)</a> <a id="278" class="Symbol">:</a> <a id="280" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="284" class="Keyword">where</a>
    18. 

  18.   <a id="List.[]"></a><a id="292" href="Issue1062.html#292" class="InductiveConstructor">[]</a> <a id="295" class="Symbol">:</a> <a id="297" href="Issue1062.html#263" class="Datatype">List</a> <a id="302" href="Issue1062.html#269" class="Bound">A</a>
    19. 

  19.   <a id="List._∷_"></a><a id="306" href="Issue1062.html#306" class="InductiveConstructor Operator">_∷_</a> <a id="310" class="Symbol">:</a> <a id="312" class="Symbol">(</a><a id="313" href="Issue1062.html#313" class="Bound">x</a> <a id="315" class="Symbol">:</a> <a id="317" href="Issue1062.html#269" class="Bound">A</a><a id="318" class="Symbol">)</a> <a id="320" class="Symbol">(</a><a id="321" href="Issue1062.html#321" class="Bound">xs</a> <a id="324" class="Symbol">:</a> <a id="326" href="Issue1062.html#263" class="Datatype">List</a> <a id="331" href="Issue1062.html#269" class="Bound">A</a><a id="332" class="Symbol">)</a> <a id="334" class="Symbol">-&gt;</a> <a id="337" href="Issue1062.html#263" class="Datatype">List</a> <a id="342" href="Issue1062.html#269" class="Bound">A</a>
    20. 

  20. 

  21. <a id="345" class="Keyword">record</a> <a id="_×_"></a><a id="352" href="Issue1062.html#352" class="Record Operator">_×_</a> <a id="356" class="Symbol">(</a><a id="357" href="Issue1062.html#357" class="Bound">A</a> <a id="359" href="Issue1062.html#359" class="Bound">B</a> <a id="361" class="Symbol">:</a> <a id="363" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="366" class="Symbol">)</a> <a id="368" class="Symbol">:</a> <a id="370" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="374" class="Keyword">where</a>
    22. 

  22.   <a id="382" class="Keyword">constructor</a> <a id="_,_"></a><a id="394" href="Issue1062.html#394" class="InductiveConstructor Operator">_,_</a>
    23. 

  23.   <a id="400" class="Keyword">field</a>
    24. 

  24.     <a id="_×_.fst"></a><a id="410" href="Issue1062.html#410" class="Field">fst</a> <a id="414" class="Symbol">:</a> <a id="416" href="Issue1062.html#357" class="Bound">A</a>
    25. 

  25.     <a id="_×_.snd"></a><a id="422" href="Issue1062.html#422" class="Field">snd</a> <a id="426" class="Symbol">:</a> <a id="428" href="Issue1062.html#359" class="Bound">B</a>
    26. 

  26. <a id="430" class="Keyword">open</a> <a id="435" href="Issue1062.html#352" class="Module Operator">_×_</a>
    27. 

  27. 

  28. <a id="440" class="Comment">-- Sized streams via head/tail.</a>
    29. 

  29. 

  30. <a id="473" class="Keyword">record</a> <a id="Stream"></a><a id="480" href="Issue1062.html#480" class="Record">Stream</a> <a id="487" class="Symbol">{</a><a id="488" href="Issue1062.html#488" class="Bound">i</a> <a id="490" class="Symbol">:</a> <a id="492" href="Issue1062.html#153" class="Postulate">Size</a><a id="496" class="Symbol">}</a> <a id="498" class="Symbol">(</a><a id="499" href="Issue1062.html#499" class="Bound">A</a> <a id="501" class="Symbol">:</a> <a id="503" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="506" class="Symbol">)</a> <a id="508" class="Symbol">:</a> <a id="510" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="514" class="Keyword">where</a>
    31. 

  31.   <a id="522" class="Keyword">coinductive</a><a id="533" class="Symbol">;</a> <a id="535" class="Keyword">constructor</a> <a id="_∷_"></a><a id="547" href="Issue1062.html#547" class="CoinductiveConstructor Operator">_∷_</a>
    32. 

  32.   <a id="553" class="Keyword">field</a>
    33. 

  33.     <a id="Stream.head"></a><a id="563" href="Issue1062.html#563" class="Field">head</a>  <a id="569" class="Symbol">:</a> <a id="571" href="Issue1062.html#499" class="Bound">A</a>
    34. 

  34.     <a id="Stream.tail"></a><a id="577" href="Issue1062.html#577" class="Field">tail</a>  <a id="583" class="Symbol">:</a> <a id="585" class="Symbol">∀</a> <a id="587" class="Symbol">{</a><a id="588" href="Issue1062.html#588" class="Bound">j</a> <a id="590" class="Symbol">:</a> <a id="592" href="Issue1062.html#184" class="Postulate Operator">Size&lt;</a> <a id="598" href="Issue1062.html#488" class="Bound">i</a><a id="599" class="Symbol">}</a> <a id="601" class="Symbol">→</a> <a id="603" href="Issue1062.html#480" class="Record">Stream</a> <a id="610" class="Symbol">{</a><a id="611" href="Issue1062.html#588" class="Bound">j</a><a id="612" class="Symbol">}</a> <a id="614" href="Issue1062.html#499" class="Bound">A</a>
    35. 

  35. <a id="616" class="Keyword">open</a> <a id="621" href="Issue1062.html#480" class="Module">Stream</a> <a id="628" class="Keyword">public</a>
    36. 

  36. 

  37. <a id="_∷ˢ_"></a><a id="636" href="Issue1062.html#636" class="Function Operator">_∷ˢ_</a> <a id="641" class="Symbol">:</a> <a id="643" class="Symbol">∀</a> <a id="645" class="Symbol">{</a><a id="646" href="Issue1062.html#646" class="Bound">i</a> <a id="648" href="Issue1062.html#648" class="Bound">A</a><a id="649" class="Symbol">}</a> <a id="651" class="Symbol">→</a> <a id="653" href="Issue1062.html#648" class="Bound">A</a> <a id="655" class="Symbol">→</a> <a id="657" href="Issue1062.html#480" class="Record">Stream</a> <a id="664" class="Symbol">{</a><a id="665" href="Issue1062.html#646" class="Bound">i</a><a id="666" class="Symbol">}</a> <a id="668" href="Issue1062.html#648" class="Bound">A</a> <a id="670" class="Symbol">→</a> <a id="672" href="Issue1062.html#480" class="Record">Stream</a> <a id="679" class="Symbol">{</a><a id="680" href="Issue1062.html#215" class="Postulate Operator">↑</a> <a id="682" href="Issue1062.html#646" class="Bound">i</a><a id="683" class="Symbol">}</a> <a id="685" href="Issue1062.html#648" class="Bound">A</a>
    38. 

  38. <a id="687" href="Issue1062.html#563" class="Field">head</a>  <a id="693" class="Symbol">(</a><a id="694" href="Issue1062.html#694" class="Bound">a</a> <a id="696" href="Issue1062.html#636" class="Function Operator">∷ˢ</a> <a id="699" href="Issue1062.html#699" class="Bound">as</a><a id="701" class="Symbol">)</a> <a id="703" class="Symbol">=</a> <a id="705" href="Issue1062.html#694" class="Bound">a</a>
    39. 

  39. <a id="707" href="Issue1062.html#577" class="Field">tail</a>  <a id="713" class="Symbol">(</a><a id="714" href="Issue1062.html#714" class="Bound">a</a> <a id="716" href="Issue1062.html#636" class="Function Operator">∷ˢ</a> <a id="719" href="Issue1062.html#719" class="Bound">as</a><a id="721" class="Symbol">)</a> <a id="723" class="Symbol">=</a> <a id="725" href="Issue1062.html#719" class="Bound">as</a>
    40. 

  40. 

  41. <a id="729" class="Comment">-- Streams and lists.</a>
    42. 

  42. 

  43. <a id="752" class="Comment">-- Prepending a list to a stream.</a>
    44. 

  44. 

  45. <a id="_++ˢ_"></a><a id="787" href="Issue1062.html#787" class="Function Operator">_++ˢ_</a> <a id="793" class="Symbol">:</a> <a id="795" class="Symbol">∀</a> <a id="797" class="Symbol">{</a><a id="798" href="Issue1062.html#798" class="Bound">i</a> <a id="800" href="Issue1062.html#800" class="Bound">A</a><a id="801" class="Symbol">}</a> <a id="803" class="Symbol">→</a> <a id="805" href="Issue1062.html#263" class="Datatype">List</a> <a id="810" href="Issue1062.html#800" class="Bound">A</a> <a id="812" class="Symbol">→</a> <a id="814" href="Issue1062.html#480" class="Record">Stream</a> <a id="821" class="Symbol">{</a><a id="822" href="Issue1062.html#798" class="Bound">i</a><a id="823" class="Symbol">}</a> <a id="825" href="Issue1062.html#800" class="Bound">A</a> <a id="827" class="Symbol">→</a> <a id="829" href="Issue1062.html#480" class="Record">Stream</a> <a id="836" class="Symbol">{</a><a id="837" href="Issue1062.html#798" class="Bound">i</a><a id="838" class="Symbol">}</a> <a id="840" href="Issue1062.html#800" class="Bound">A</a>
    46. 

  46. <a id="842" href="Issue1062.html#292" class="InductiveConstructor">[]</a>        <a id="852" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="856" href="Issue1062.html#856" class="Bound">s</a> <a id="858" class="Symbol">=</a> <a id="860" href="Issue1062.html#856" class="Bound">s</a>
    47. 

  47. <a id="862" class="Symbol">(</a><a id="863" href="Issue1062.html#863" class="Bound">a</a> <a id="865" href="Issue1062.html#306" class="InductiveConstructor Operator">∷</a> <a id="867" href="Issue1062.html#867" class="Bound">as</a><a id="869" class="Symbol">)</a>  <a id="872" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="876" href="Issue1062.html#876" class="Bound">s</a> <a id="878" class="Symbol">=</a> <a id="880" href="Issue1062.html#863" class="Bound">a</a> <a id="882" href="Issue1062.html#636" class="Function Operator">∷ˢ</a> <a id="885" class="Symbol">(</a><a id="886" href="Issue1062.html#867" class="Bound">as</a> <a id="889" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="893" href="Issue1062.html#876" class="Bound">s</a><a id="894" class="Symbol">)</a>
    48. 

  48. 

  49. <a id="897" class="Comment">-- Unfold which produces several outputs at one step</a>
    50. 

  50. 

  51. <a id="951" class="Keyword">record</a> <a id="List1"></a><a id="958" href="Issue1062.html#958" class="Record">List1</a> <a id="964" class="Symbol">(</a><a id="965" href="Issue1062.html#965" class="Bound">A</a> <a id="967" class="Symbol">:</a> <a id="969" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="972" class="Symbol">)</a> <a id="974" class="Symbol">:</a> <a id="976" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="980" class="Keyword">where</a>
    52. 

  52.   <a id="988" class="Keyword">constructor</a> <a id="_∷_"></a><a id="1000" href="Issue1062.html#1000" class="InductiveConstructor Operator">_∷_</a>
    53. 

  53.   <a id="1006" class="Keyword">field</a>
    54. 

  54.     <a id="List1.head"></a><a id="1016" href="Issue1062.html#1016" class="Field">head</a>  <a id="1022" class="Symbol">:</a> <a id="1024" href="Issue1062.html#965" class="Bound">A</a>
    55. 

  55.     <a id="List1.tail"></a><a id="1030" href="Issue1062.html#1030" class="Field">tail</a>  <a id="1036" class="Symbol">:</a> <a id="1038" href="Issue1062.html#263" class="Datatype">List</a> <a id="1043" href="Issue1062.html#965" class="Bound">A</a>
    56. 

  56. <a id="1045" class="Keyword">open</a> <a id="1050" href="Issue1062.html#958" class="Module">List1</a> <a id="1056" class="Keyword">using</a> <a id="1062" class="Symbol">(</a><a id="1063" href="Issue1062.html#1016" class="Field">head</a><a id="1067" class="Symbol">;</a> <a id="1069" href="Issue1062.html#1030" class="Field">tail</a><a id="1073" class="Symbol">)</a>
    57. 

  57. 

  58. <a id="1076" class="Keyword">record</a> <a id="⊤"></a><a id="1083" href="Issue1062.html#1083" class="Record">⊤</a> <a id="1085" class="Symbol">:</a> <a id="1087" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="1091" class="Keyword">where</a> <a id="1097" class="Keyword">constructor</a> <a id="trivial"></a><a id="1109" href="Issue1062.html#1109" class="InductiveConstructor">trivial</a>
    59. 

  59. <a id="1117" class="Keyword">open</a> <a id="1122" href="Issue1062.html#958" class="Module">List1</a> <a id="1128" class="Symbol">(</a><a id="1129" href="Issue1062.html#1109" class="InductiveConstructor">trivial</a> <a id="1137" href="Issue1062.html#1000" class="InductiveConstructor Operator">∷</a> <a id="1139" href="Issue1062.html#292" class="InductiveConstructor">[]</a><a id="1141" class="Symbol">)</a> <a id="1143" class="Keyword">using</a> <a id="1149" class="Symbol">(</a><a id="1150" href="Issue1062.html#1016" class="Field">head</a><a id="1154" class="Symbol">;</a> <a id="1156" href="Issue1062.html#1030" class="Field">tail</a><a id="1160" class="Symbol">)</a> <a id="1162" class="Comment">-- problem: imports not colored</a>
    60. 

  60. 

  61. <a id="unfold⁺"></a><a id="1195" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1203" class="Symbol">:</a> <a id="1205" class="Symbol">∀</a> <a id="1207" class="Symbol">{</a><a id="1208" href="Issue1062.html#1208" class="Bound">S</a> <a id="1210" class="Symbol">:</a> <a id="1212" href="Issue1062.html#153" class="Postulate">Size</a> <a id="1217" class="Symbol">→</a> <a id="1219" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="1222" class="Symbol">}</a> <a id="1224" class="Symbol">{</a><a id="1225" href="Issue1062.html#1225" class="Bound">A</a> <a id="1227" class="Symbol">:</a> <a id="1229" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="1232" class="Symbol">}</a>
    62. 

  62. 

  63.   <a id="1237" class="Symbol">(</a><a id="1238" href="Issue1062.html#1238" class="Bound">step</a> <a id="1243" class="Symbol">:</a> <a id="1245" class="Symbol">∀</a> <a id="1247" class="Symbol">{</a><a id="1248" href="Issue1062.html#1248" class="Bound">i</a><a id="1249" class="Symbol">}</a> <a id="1251" class="Symbol">→</a> <a id="1253" href="Issue1062.html#1208" class="Bound">S</a> <a id="1255" href="Issue1062.html#1248" class="Bound">i</a> <a id="1257" class="Symbol">→</a> <a id="1259" href="Issue1062.html#958" class="Record">List1</a> <a id="1265" href="Issue1062.html#1225" class="Bound">A</a> <a id="1267" href="Issue1062.html#352" class="Record Operator">×</a> <a id="1269" class="Symbol">(∀</a> <a id="1272" class="Symbol">{</a><a id="1273" href="Issue1062.html#1273" class="Bound">j</a> <a id="1275" class="Symbol">:</a> <a id="1277" href="Issue1062.html#184" class="Postulate Operator">Size&lt;</a> <a id="1283" href="Issue1062.html#1248" class="Bound">i</a><a id="1284" class="Symbol">}</a> <a id="1286" class="Symbol">→</a> <a id="1288" href="Issue1062.html#1208" class="Bound">S</a> <a id="1290" href="Issue1062.html#1273" class="Bound">j</a><a id="1291" class="Symbol">))</a> <a id="1294" class="Symbol">→</a>
    64. 

  64. 

  65.   <a id="1299" class="Symbol">∀</a> <a id="1301" class="Symbol">{</a><a id="1302" href="Issue1062.html#1302" class="Bound">i</a><a id="1303" class="Symbol">}</a> <a id="1305" class="Symbol">→</a> <a id="1307" class="Symbol">(</a><a id="1308" href="Issue1062.html#1308" class="Bound">s</a> <a id="1310" class="Symbol">:</a> <a id="1312" href="Issue1062.html#1208" class="Bound">S</a> <a id="1314" href="Issue1062.html#1302" class="Bound">i</a><a id="1315" class="Symbol">)</a> <a id="1317" class="Symbol">→</a> <a id="1319" href="Issue1062.html#480" class="Record">Stream</a> <a id="1326" class="Symbol">{</a><a id="1327" href="Issue1062.html#1302" class="Bound">i</a><a id="1328" class="Symbol">}</a> <a id="1330" href="Issue1062.html#1225" class="Bound">A</a>
    66. 

  66. 

  67. <a id="1333" href="Issue1062.html#563" class="Field">head</a>  <a id="1339" class="Symbol">(</a><a id="1340" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1348" href="Issue1062.html#1348" class="Bound">step</a> <a id="1353" href="Issue1062.html#1353" class="Bound">s</a><a id="1354" class="Symbol">)</a> <a id="1356" class="Symbol">=</a>  <a id="1359" href="Issue1062.html#1016" class="Field">head</a> <a id="1364" class="Symbol">(</a><a id="1365" href="Issue1062.html#410" class="Field">fst</a> <a id="1369" class="Symbol">(</a><a id="1370" href="Issue1062.html#1348" class="Bound">step</a> <a id="1375" href="Issue1062.html#1353" class="Bound">s</a><a id="1376" class="Symbol">))</a>
    68. 

  68. <a id="1379" href="Issue1062.html#577" class="Field">tail</a>  <a id="1385" class="Symbol">(</a><a id="1386" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1394" href="Issue1062.html#1394" class="Bound">step</a> <a id="1399" href="Issue1062.html#1399" class="Bound">s</a><a id="1400" class="Symbol">)</a> <a id="1402" class="Symbol">=</a>  <a id="1405" class="Keyword">let</a>  <a id="1410" class="Symbol">((_</a> <a id="1414" href="Issue1062.html#1000" class="InductiveConstructor Operator">∷</a> <a id="1416" href="Issue1062.html#1416" class="Bound">l</a><a id="1417" class="Symbol">)</a> <a id="1419" href="Issue1062.html#394" class="InductiveConstructor Operator">,</a> <a id="1421" href="Issue1062.html#1421" class="Bound">s′</a><a id="1423" class="Symbol">)</a> <a id="1425" class="Symbol">=</a> <a id="1427" href="Issue1062.html#1394" class="Bound">step</a> <a id="1432" href="Issue1062.html#1399" class="Bound">s</a>
    69. 

  69.                           <a id="1460" class="Keyword">in</a>   <a id="1465" href="Issue1062.html#1416" class="Bound">l</a> <a id="1467" href="Issue1062.html#787" class="Function Operator">++ˢ</a> <a id="1471" href="Issue1062.html#1195" class="Function">unfold⁺</a> <a id="1479" href="Issue1062.html#1394" class="Bound">step</a> <a id="1484" href="Issue1062.html#1421" class="Bound">s′</a>
    70. 

  70. <a id="1487" class="Markup">\end{code}</a><a id="1497" class="Background">
    71. 

  71. Problem: The ∷ in the last let statement is not colored with constructor color.
    72. 

  72. \end{document}
    73. 

  73. </a></pre></body></html>
    74.