Home Explore Help
Sign In
caryoscelus
/
agda
Watch 1
Star 0
Fork 0
Files Issues 0 Pull Requests 0 Wiki
Tree: ce9b406819
Branches Tags
agda
/
test
/
LaTeXAndHTML
/
succeed
/
MdJustHighlightAgdaAsHtml.html

MdJustHighlightAgdaAsHtml.html 16 KB
History Raw

123456789101112131415161718192021222324252627282930313233343536373839404142434445 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>MdJustHighlightAgdaAsHtml</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- A discussion from -- https://twitter.com/YuumuKonpaku/status/1052959340468953088</a>
    3. 

  3. <a id="85" class="Comment">-- Andreas, 2019-08-18, test also #1346 (infix declaration in renaming)</a>
    4. 

  4. <a id="157" class="Comment">-- Andreas, 2019-02-17, test alse #3432 (pattern synonyms in import directive)</a>
    5. 

  5. 

  6. <a id="237" class="Keyword">module</a> <a id="244" href="MdJustHighlightAgdaAsHtml.html" class="Module">MdJustHighlightAgdaAsHtml</a> <a id="270" class="Keyword">where</a>
    7. 

  7. 

  8. <a id="277" class="Keyword">open</a> <a id="282" class="Keyword">import</a> <a id="289" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
    9. 

  9. <a id="306" class="Keyword">open</a> <a id="311" class="Keyword">import</a> <a id="318" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>
    10. 

  10. <a id="340" class="Keyword">open</a> <a id="345" class="Keyword">import</a> <a id="352" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="367" class="Keyword">public</a> <a id="374" class="Keyword">using</a> <a id="380" class="Symbol">(</a><a id="381" href="Agda.Primitive.html#749" class="Primitive">lzero</a><a id="386" class="Symbol">)</a>
    11. 

  11.   <a id="390" class="Keyword">renaming</a> <a id="399" class="Symbol">(</a><a id="400" href="Agda.Primitive.html#582" class="Postulate">Level</a> <a id="406" class="Symbol">to</a> <a id="409" class="Postulate">ULevel</a><a id="415" class="Symbol">;</a> <a id="417" href="Agda.Primitive.html#765" class="Primitive">lsuc</a> <a id="422" class="Symbol">to</a> <a id="425" class="Primitive">lsucc</a><a id="430" class="Symbol">;</a> <a id="432" href="Agda.Primitive.html#795" class="Primitive Operator">_⊔_</a> <a id="436" class="Symbol">to</a> <a id="439" class="Keyword">infixl</a> <a id="446" class="Number">42</a> <a id="449" class="Primitive Operator">_⊔_</a><a id="452" class="Symbol">)</a>
    12. 

  12. 

  13. <a id="Type"></a><a id="455" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="460" class="Symbol">:</a> <a id="462" class="Symbol">(</a><a id="463" href="MdJustHighlightAgdaAsHtml.html#463" class="Bound">i</a> <a id="465" class="Symbol">:</a> <a id="467" href="MdJustHighlightAgdaAsHtml.html#409" class="Postulate">ULevel</a><a id="473" class="Symbol">)</a> <a id="475" class="Symbol">-&gt;</a> <a id="478" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="482" class="Symbol">(</a><a id="483" href="MdJustHighlightAgdaAsHtml.html#425" class="Primitive">lsucc</a> <a id="489" href="MdJustHighlightAgdaAsHtml.html#463" class="Bound">i</a><a id="490" class="Symbol">)</a>
    14. 

  14. <a id="492" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="497" href="MdJustHighlightAgdaAsHtml.html#497" class="Bound">i</a> <a id="499" class="Symbol">=</a> <a id="501" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="505" href="MdJustHighlightAgdaAsHtml.html#497" class="Bound">i</a>
    15. 

  15. 

  16. <a id="508" class="Keyword">data</a> <a id="⊥"></a><a id="513" href="MdJustHighlightAgdaAsHtml.html#513" class="Datatype">⊥</a> <a id="515" class="Symbol">:</a> <a id="517" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="522" href="Agda.Primitive.html#749" class="Primitive">lzero</a> <a id="528" class="Keyword">where</a>
    17. 

  17. 

  18. <a id="535" class="Keyword">module</a> <a id="PatternSyns"></a><a id="542" href="MdJustHighlightAgdaAsHtml.html#542" class="Module">PatternSyns</a> <a id="554" class="Keyword">where</a>
    19. 

  19.   <a id="562" class="Keyword">pattern</a> <a id="PatternSyns.O&#39;"></a><a id="570" href="MdJustHighlightAgdaAsHtml.html#570" class="InductiveConstructor">O&#39;</a> <a id="573" class="Symbol">=</a> <a id="575" href="Agda.Builtin.Nat.html#195" class="InductiveConstructor">zero</a>
    20. 

  20.   <a id="582" class="Keyword">pattern</a> <a id="PatternSyns.S"></a><a id="590" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="592" href="MdJustHighlightAgdaAsHtml.html#601" class="Bound">n</a> <a id="594" class="Symbol">=</a> <a id="596" class="Symbol">(</a><a id="597" href="Agda.Builtin.Nat.html#208" class="InductiveConstructor">suc</a> <a id="601" href="MdJustHighlightAgdaAsHtml.html#601" class="Bound">n</a><a id="602" class="Symbol">)</a>
    21. 

  21. <a id="604" class="Keyword">open</a> <a id="609" href="MdJustHighlightAgdaAsHtml.html#542" class="Module">PatternSyns</a> <a id="621" class="Keyword">using</a> <a id="627" class="Symbol">(</a><a id="628" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a><a id="629" class="Symbol">)</a> <a id="631" class="Keyword">renaming</a> <a id="640" class="Symbol">(</a><a id="641" href="MdJustHighlightAgdaAsHtml.html#570" class="InductiveConstructor">O&#39;</a> <a id="644" class="Symbol">to</a> <a id="647" class="InductiveConstructor">O</a><a id="648" class="Symbol">)</a>
    22. 

  22. 

  23. <a id="651" class="Keyword">variable</a> <a id="660" href="MdJustHighlightAgdaAsHtml.html#660" class="Generalizable">i</a> <a id="662" class="Symbol">:</a> <a id="664" href="MdJustHighlightAgdaAsHtml.html#409" class="Postulate">ULevel</a>
    24. 

  24. 

  25. <a id="¬"></a><a id="672" href="MdJustHighlightAgdaAsHtml.html#672" class="Function">¬</a> <a id="674" class="Symbol">:</a> <a id="676" class="Symbol">(</a><a id="677" href="MdJustHighlightAgdaAsHtml.html#677" class="Bound">A</a> <a id="679" class="Symbol">:</a> <a id="681" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="686" href="MdJustHighlightAgdaAsHtml.html#660" class="Generalizable">i</a><a id="687" class="Symbol">)</a> <a id="689" class="Symbol">→</a> <a id="691" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="696" href="MdJustHighlightAgdaAsHtml.html#660" class="Generalizable">i</a>
    26. 

  26. <a id="698" href="MdJustHighlightAgdaAsHtml.html#672" class="Function">¬</a> <a id="700" href="MdJustHighlightAgdaAsHtml.html#700" class="Bound">A</a> <a id="702" class="Symbol">=</a> <a id="704" href="MdJustHighlightAgdaAsHtml.html#700" class="Bound">A</a> <a id="706" class="Symbol">→</a> <a id="708" href="MdJustHighlightAgdaAsHtml.html#513" class="Datatype">⊥</a>
    27. 

  27. <a id="_≠_"></a><a id="710" href="MdJustHighlightAgdaAsHtml.html#710" class="Function Operator">_≠_</a> <a id="714" class="Symbol">:</a> <a id="716" class="Symbol">{</a><a id="717" href="MdJustHighlightAgdaAsHtml.html#717" class="Bound">A</a> <a id="719" class="Symbol">:</a> <a id="721" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="726" href="MdJustHighlightAgdaAsHtml.html#660" class="Generalizable">i</a><a id="727" class="Symbol">}</a> <a id="729" class="Symbol">→</a> <a id="731" class="Symbol">(</a><a id="732" href="MdJustHighlightAgdaAsHtml.html#717" class="Bound">A</a> <a id="734" class="Symbol">→</a> <a id="736" href="MdJustHighlightAgdaAsHtml.html#717" class="Bound">A</a> <a id="738" class="Symbol">→</a> <a id="740" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="745" href="MdJustHighlightAgdaAsHtml.html#660" class="Generalizable">i</a><a id="746" class="Symbol">)</a>
    28. 

  28. <a id="748" href="MdJustHighlightAgdaAsHtml.html#748" class="Bound">x</a> <a id="750" href="MdJustHighlightAgdaAsHtml.html#710" class="Function Operator">≠</a> <a id="752" href="MdJustHighlightAgdaAsHtml.html#752" class="Bound">y</a> <a id="754" class="Symbol">=</a> <a id="756" href="MdJustHighlightAgdaAsHtml.html#672" class="Function">¬</a> <a id="758" class="Symbol">(</a><a id="759" href="MdJustHighlightAgdaAsHtml.html#748" class="Bound">x</a> <a id="761" href="Agda.Builtin.Equality.html#124" class="Datatype Operator">≡</a> <a id="763" href="MdJustHighlightAgdaAsHtml.html#752" class="Bound">y</a><a id="764" class="Symbol">)</a>
    29. 

  29. 

  30. <a id="767" class="Keyword">infix</a> <a id="773" class="Number">10</a> <a id="776" href="MdJustHighlightAgdaAsHtml.html#785" class="Datatype Operator">_∨_</a>
    31. 

  31. <a id="780" class="Keyword">data</a> <a id="_∨_"></a><a id="785" href="MdJustHighlightAgdaAsHtml.html#785" class="Datatype Operator">_∨_</a> <a id="789" class="Symbol">{</a><a id="790" href="MdJustHighlightAgdaAsHtml.html#790" class="Bound">a</a> <a id="792" href="MdJustHighlightAgdaAsHtml.html#792" class="Bound">b</a><a id="793" class="Symbol">}</a> <a id="795" class="Symbol">(</a><a id="796" href="MdJustHighlightAgdaAsHtml.html#796" class="Bound">A</a> <a id="798" class="Symbol">:</a> <a id="800" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="805" href="MdJustHighlightAgdaAsHtml.html#790" class="Bound">a</a><a id="806" class="Symbol">)</a> <a id="808" class="Symbol">(</a><a id="809" href="MdJustHighlightAgdaAsHtml.html#809" class="Bound">B</a> <a id="811" class="Symbol">:</a> <a id="813" href="MdJustHighlightAgdaAsHtml.html#455" class="Function">Type</a> <a id="818" href="MdJustHighlightAgdaAsHtml.html#792" class="Bound">b</a><a id="819" class="Symbol">)</a> <a id="821" class="Symbol">:</a> <a id="823" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="827" class="Symbol">(</a><a id="828" href="MdJustHighlightAgdaAsHtml.html#790" class="Bound">a</a> <a id="830" href="MdJustHighlightAgdaAsHtml.html#449" class="Primitive Operator">⊔</a> <a id="832" href="MdJustHighlightAgdaAsHtml.html#792" class="Bound">b</a><a id="833" class="Symbol">)</a> <a id="835" class="Keyword">where</a>
    32. 

  32.   <a id="_∨_.a-intro"></a><a id="843" href="MdJustHighlightAgdaAsHtml.html#843" class="InductiveConstructor">a-intro</a> <a id="851" class="Symbol">:</a> <a id="853" href="MdJustHighlightAgdaAsHtml.html#796" class="Bound">A</a> <a id="855" class="Symbol">-&gt;</a> <a id="858" href="MdJustHighlightAgdaAsHtml.html#796" class="Bound">A</a> <a id="860" href="MdJustHighlightAgdaAsHtml.html#785" class="Datatype Operator">∨</a> <a id="862" href="MdJustHighlightAgdaAsHtml.html#809" class="Bound">B</a>
    33. 

  33.   <a id="_∨_.b-intro"></a><a id="866" href="MdJustHighlightAgdaAsHtml.html#866" class="InductiveConstructor">b-intro</a> <a id="874" class="Symbol">:</a> <a id="876" href="MdJustHighlightAgdaAsHtml.html#809" class="Bound">B</a> <a id="878" class="Symbol">-&gt;</a> <a id="881" href="MdJustHighlightAgdaAsHtml.html#796" class="Bound">A</a> <a id="883" href="MdJustHighlightAgdaAsHtml.html#785" class="Datatype Operator">∨</a> <a id="885" href="MdJustHighlightAgdaAsHtml.html#809" class="Bound">B</a>
    34. 

  34. 

  35. <a id="test"></a><a id="888" href="MdJustHighlightAgdaAsHtml.html#888" class="Function">test</a> <a id="893" class="Symbol">:</a> <a id="895" class="Symbol">(</a><a id="896" href="MdJustHighlightAgdaAsHtml.html#896" class="Bound">x</a> <a id="898" href="MdJustHighlightAgdaAsHtml.html#898" class="Bound">y</a> <a id="900" class="Symbol">:</a> <a id="902" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a><a id="905" class="Symbol">)</a> <a id="907" class="Symbol">-&gt;</a> <a id="910" class="Symbol">(</a><a id="911" href="MdJustHighlightAgdaAsHtml.html#896" class="Bound">x</a> <a id="913" href="Agda.Builtin.Equality.html#124" class="Datatype Operator">≡</a> <a id="915" href="MdJustHighlightAgdaAsHtml.html#898" class="Bound">y</a><a id="916" class="Symbol">)</a> <a id="918" href="MdJustHighlightAgdaAsHtml.html#785" class="Datatype Operator">∨</a> <a id="920" class="Symbol">(</a><a id="921" href="MdJustHighlightAgdaAsHtml.html#896" class="Bound">x</a> <a id="923" href="MdJustHighlightAgdaAsHtml.html#710" class="Function Operator">≠</a> <a id="925" href="MdJustHighlightAgdaAsHtml.html#898" class="Bound">y</a><a id="926" class="Symbol">)</a>
    36. 

  36. <a id="928" href="MdJustHighlightAgdaAsHtml.html#888" class="Function">test</a> <a id="933" href="MdJustHighlightAgdaAsHtml.html#647" class="InductiveConstructor">O</a> <a id="935" href="MdJustHighlightAgdaAsHtml.html#647" class="InductiveConstructor">O</a> <a id="937" class="Symbol">=</a> <a id="939" href="MdJustHighlightAgdaAsHtml.html#843" class="InductiveConstructor">a-intro</a> <a id="947" href="Agda.Builtin.Equality.html#181" class="InductiveConstructor">refl</a>
    37. 

  37. <a id="952" href="MdJustHighlightAgdaAsHtml.html#888" class="Function">test</a> <a id="957" href="MdJustHighlightAgdaAsHtml.html#647" class="InductiveConstructor">O</a> <a id="959" class="Symbol">(</a><a id="960" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="962" href="MdJustHighlightAgdaAsHtml.html#962" class="Bound">y</a><a id="963" class="Symbol">)</a> <a id="965" class="Symbol">=</a> <a id="967" href="MdJustHighlightAgdaAsHtml.html#866" class="InductiveConstructor">b-intro</a> <a id="975" class="Symbol">(λ</a> <a id="978" class="Symbol">())</a>
    38. 

  38. <a id="982" href="MdJustHighlightAgdaAsHtml.html#888" class="Function">test</a> <a id="987" class="Symbol">(</a><a id="988" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="990" href="MdJustHighlightAgdaAsHtml.html#990" class="Bound">x</a><a id="991" class="Symbol">)</a> <a id="993" href="MdJustHighlightAgdaAsHtml.html#647" class="InductiveConstructor">O</a> <a id="995" class="Symbol">=</a> <a id="997" href="MdJustHighlightAgdaAsHtml.html#866" class="InductiveConstructor">b-intro</a> <a id="1005" class="Symbol">(λ</a> <a id="1008" class="Symbol">())</a>
    39. 

  39. <a id="1012" href="MdJustHighlightAgdaAsHtml.html#888" class="Function">test</a> <a id="1017" class="Symbol">(</a><a id="1018" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="1020" href="MdJustHighlightAgdaAsHtml.html#1020" class="Bound">x</a><a id="1021" class="Symbol">)</a> <a id="1023" class="Symbol">(</a><a id="1024" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="1026" href="MdJustHighlightAgdaAsHtml.html#1026" class="Bound">y</a><a id="1027" class="Symbol">)</a> <a id="1029" class="Keyword">with</a> <a id="1034" href="MdJustHighlightAgdaAsHtml.html#888" class="Function">test</a> <a id="1039" href="MdJustHighlightAgdaAsHtml.html#1020" class="Bound">x</a> <a id="1041" href="MdJustHighlightAgdaAsHtml.html#1026" class="Bound">y</a>
    40. 

  40. <a id="1043" class="Symbol">...</a> <a id="1047" class="Symbol">|</a> <a id="1049" href="MdJustHighlightAgdaAsHtml.html#843" class="InductiveConstructor">a-intro</a> <a id="1057" href="Agda.Builtin.Equality.html#181" class="InductiveConstructor">refl</a> <a id="1062" class="Symbol">=</a> <a id="1064" href="MdJustHighlightAgdaAsHtml.html#843" class="InductiveConstructor">a-intro</a> <a id="1072" href="Agda.Builtin.Equality.html#181" class="InductiveConstructor">refl</a>
    41. 

  41. <a id="1077" class="Symbol">...</a> <a id="1081" class="Symbol">|</a> <a id="1083" href="MdJustHighlightAgdaAsHtml.html#866" class="InductiveConstructor">b-intro</a> <a id="1091" href="MdJustHighlightAgdaAsHtml.html#1091" class="Bound">k</a> <a id="1093" class="Symbol">=</a> <a id="1095" href="MdJustHighlightAgdaAsHtml.html#866" class="InductiveConstructor">b-intro</a> <a id="1103" class="Symbol">(</a><a id="1104" href="MdJustHighlightAgdaAsHtml.html#1125" class="Function">lemma</a> <a id="1110" href="MdJustHighlightAgdaAsHtml.html#1091" class="Bound">k</a><a id="1111" class="Symbol">)</a>
    42. 

  42.   <a id="1115" class="Keyword">where</a>
    43. 

  43.     <a id="1125" href="MdJustHighlightAgdaAsHtml.html#1125" class="Function">lemma</a> <a id="1131" class="Symbol">:</a> <a id="1133" class="Symbol">{</a><a id="1134" href="MdJustHighlightAgdaAsHtml.html#1134" class="Bound">a</a> <a id="1136" href="MdJustHighlightAgdaAsHtml.html#1136" class="Bound">b</a> <a id="1138" class="Symbol">:</a> <a id="1140" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a><a id="1143" class="Symbol">}</a> <a id="1145" class="Symbol">-&gt;</a> <a id="1148" href="MdJustHighlightAgdaAsHtml.html#1134" class="Bound">a</a> <a id="1150" href="MdJustHighlightAgdaAsHtml.html#710" class="Function Operator">≠</a> <a id="1152" href="MdJustHighlightAgdaAsHtml.html#1136" class="Bound">b</a> <a id="1154" class="Symbol">-&gt;</a> <a id="1157" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="1159" href="MdJustHighlightAgdaAsHtml.html#1134" class="Bound">a</a> <a id="1161" href="MdJustHighlightAgdaAsHtml.html#710" class="Function Operator">≠</a> <a id="1163" href="MdJustHighlightAgdaAsHtml.html#590" class="InductiveConstructor">S</a> <a id="1165" href="MdJustHighlightAgdaAsHtml.html#1136" class="Bound">b</a>
    44. 

  44.     <a id="1171" href="MdJustHighlightAgdaAsHtml.html#1125" class="Function">lemma</a> <a id="1177" href="MdJustHighlightAgdaAsHtml.html#1177" class="Bound">p</a> <a id="1179" href="Agda.Builtin.Equality.html#181" class="InductiveConstructor">refl</a> <a id="1184" class="Symbol">=</a> <a id="1186" href="MdJustHighlightAgdaAsHtml.html#1177" class="Bound">p</a> <a id="1188" href="Agda.Builtin.Equality.html#181" class="InductiveConstructor">refl</a>
    45. 

  45. </pre></body></html>
    46.