Domovská stránka Prehľadávať Pomoc
Prihlásiť sa
caryoscelus
/
agda
Pridať medzi pozorované 1
Hviezda 0
Fork 0
Súbory Issues 0 Pull requesty 0 Wiki
Strom: ce9b406819
Branche Tagy
agda
/
test
/
LaTeXAndHTML
/
succeed
/
Issue4580NegativeLiterals.html

Issue4580NegativeLiterals.html 8.2 KB
História Raw

12345678910111213141516171819202122232425262728293031323334353637383940 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>Issue4580NegativeLiterals</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- Andreas, 2020-04-12, issue #4580</a>
    3. 

  3. <a id="37" class="Comment">-- Highlighting for builtins FROMNAT, FROMNEG, FROMSTRING</a>
    4. 

  4. 

  5. <a id="96" class="Keyword">open</a> <a id="101" class="Keyword">import</a> <a id="108" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
    6. 

  6. <a id="125" class="Keyword">open</a> <a id="130" class="Keyword">import</a> <a id="137" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a>
    7. 

  7. 

  8. <a id="160" class="Keyword">record</a> <a id="Number"></a><a id="167" href="Issue4580NegativeLiterals.html#167" class="Record">Number</a> <a id="174" class="Symbol">(</a><a id="175" href="Issue4580NegativeLiterals.html#175" class="Bound">A</a> <a id="177" class="Symbol">:</a> <a id="179" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="182" class="Symbol">)</a> <a id="184" class="Symbol">:</a> <a id="186" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="190" class="Keyword">where</a>
    9. 

  9.   <a id="198" class="Keyword">field</a> <a id="Number.fromNat"></a><a id="204" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="212" class="Symbol">:</a> <a id="214" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a> <a id="218" class="Symbol">→</a> <a id="220" href="Issue4580NegativeLiterals.html#175" class="Bound">A</a>
    10. 

  10. 

  11. <a id="223" class="Keyword">record</a> <a id="Negative"></a><a id="230" href="Issue4580NegativeLiterals.html#230" class="Record">Negative</a> <a id="239" class="Symbol">(</a><a id="240" href="Issue4580NegativeLiterals.html#240" class="Bound">A</a> <a id="242" class="Symbol">:</a> <a id="244" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="247" class="Symbol">)</a> <a id="249" class="Symbol">:</a> <a id="251" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="255" class="Keyword">where</a>
    12. 

  12.   <a id="263" class="Keyword">field</a> <a id="Negative.fromNeg"></a><a id="269" href="Issue4580NegativeLiterals.html#269" class="Field">fromNeg</a> <a id="277" class="Symbol">:</a> <a id="279" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a> <a id="283" class="Symbol">→</a> <a id="285" href="Issue4580NegativeLiterals.html#240" class="Bound">A</a>
    13. 

  13. 

  14. <a id="288" class="Keyword">open</a> <a id="293" href="Issue4580NegativeLiterals.html#167" class="Module">Number</a> <a id="300" class="Symbol">{{...}}</a> <a id="308" class="Keyword">public</a>
    15. 

  15. <a id="315" class="Keyword">open</a> <a id="320" href="Issue4580NegativeLiterals.html#230" class="Module">Negative</a> <a id="329" class="Symbol">{{...}}</a> <a id="337" class="Keyword">public</a>
    16. 

  16. 

  17. <a id="345" class="Symbol">{-#</a> <a id="349" class="Keyword">BUILTIN</a> <a id="357" class="Keyword">FROMNAT</a> <a id="365" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="373" class="Symbol">#-}</a>  <a id="378" class="Comment">-- Should be highlighted.</a>
    18. 

  18. <a id="404" class="Symbol">{-#</a> <a id="408" class="Keyword">BUILTIN</a> <a id="416" class="Keyword">FROMNEG</a> <a id="424" href="Issue4580NegativeLiterals.html#269" class="Field">fromNeg</a> <a id="432" class="Symbol">#-}</a>  <a id="437" class="Comment">-- Jump to definition should work.</a>
    19. 

  19. 

  20. <a id="473" class="Keyword">instance</a>
    21. 

  21.   <a id="NumberNat"></a><a id="484" href="Issue4580NegativeLiterals.html#484" class="Function">NumberNat</a> <a id="494" class="Symbol">:</a> <a id="496" href="Issue4580NegativeLiterals.html#167" class="Record">Number</a> <a id="503" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a>
    22. 

  22.   <a id="509" href="Issue4580NegativeLiterals.html#484" class="Function">NumberNat</a> <a id="519" class="Symbol">=</a> <a id="521" class="Keyword">record</a> <a id="528" class="Symbol">{</a> <a id="530" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="538" class="Symbol">=</a> <a id="540" class="Symbol">λ</a> <a id="542" href="Issue4580NegativeLiterals.html#542" class="Bound">n</a> <a id="544" class="Symbol">→</a> <a id="546" href="Issue4580NegativeLiterals.html#542" class="Bound">n</a> <a id="548" class="Symbol">}</a>
    23. 

  23. 

  24. <a id="551" class="Keyword">data</a> <a id="Int"></a><a id="556" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a> <a id="560" class="Symbol">:</a> <a id="562" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="566" class="Keyword">where</a>
    25. 

  25.   <a id="Int.pos"></a><a id="574" href="Issue4580NegativeLiterals.html#574" class="InductiveConstructor">pos</a> <a id="578" class="Symbol">:</a> <a id="580" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a> <a id="584" class="Symbol">→</a> <a id="586" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
    26. 

  26.   <a id="Int.neg"></a><a id="592" href="Issue4580NegativeLiterals.html#592" class="InductiveConstructor">neg</a> <a id="596" class="Symbol">:</a> <a id="598" href="Agda.Builtin.Nat.html#177" class="Datatype">Nat</a> <a id="602" class="Symbol">→</a> <a id="604" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
    27. 

  27. 

  28. <a id="609" class="Keyword">instance</a>
    29. 

  29.   <a id="NumberInt"></a><a id="620" href="Issue4580NegativeLiterals.html#620" class="Function">NumberInt</a> <a id="630" class="Symbol">:</a> <a id="632" href="Issue4580NegativeLiterals.html#167" class="Record">Number</a> <a id="639" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
    30. 

  30.   <a id="645" href="Issue4580NegativeLiterals.html#620" class="Function">NumberInt</a> <a id="655" class="Symbol">=</a> <a id="657" class="Keyword">record</a> <a id="664" class="Symbol">{</a> <a id="666" href="Issue4580NegativeLiterals.html#204" class="Field">fromNat</a> <a id="674" class="Symbol">=</a> <a id="676" href="Issue4580NegativeLiterals.html#574" class="InductiveConstructor">pos</a> <a id="680" class="Symbol">}</a>
    31. 

  31. 

  32.   <a id="NegativeInt"></a><a id="685" href="Issue4580NegativeLiterals.html#685" class="Function">NegativeInt</a> <a id="697" class="Symbol">:</a> <a id="699" href="Issue4580NegativeLiterals.html#230" class="Record">Negative</a> <a id="708" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
    33. 

  33.   <a id="714" href="Issue4580NegativeLiterals.html#685" class="Function">NegativeInt</a> <a id="726" class="Symbol">=</a> <a id="728" class="Keyword">record</a> <a id="735" class="Symbol">{</a> <a id="737" href="Issue4580NegativeLiterals.html#269" class="Field">fromNeg</a> <a id="745" class="Symbol">=</a> <a id="747" class="Symbol">λ</a> <a id="749" class="Symbol">{</a> <a id="751" href="Agda.Builtin.Nat.html#195" class="InductiveConstructor">zero</a> <a id="756" class="Symbol">→</a> <a id="758" href="Issue4580NegativeLiterals.html#574" class="InductiveConstructor">pos</a> <a id="762" class="Number">0</a> <a id="764" class="Symbol">;</a> <a id="766" class="Symbol">(</a><a id="767" href="Agda.Builtin.Nat.html#208" class="InductiveConstructor">suc</a> <a id="771" href="Issue4580NegativeLiterals.html#771" class="Bound">n</a><a id="772" class="Symbol">)</a> <a id="774" class="Symbol">→</a> <a id="776" href="Issue4580NegativeLiterals.html#592" class="InductiveConstructor">neg</a> <a id="780" href="Issue4580NegativeLiterals.html#771" class="Bound">n</a> <a id="782" class="Symbol">}</a> <a id="784" class="Symbol">}</a>
    34. 

  34. 

  35. <a id="minusFive"></a><a id="787" href="Issue4580NegativeLiterals.html#787" class="Function">minusFive</a> <a id="797" class="Symbol">:</a> <a id="799" href="Issue4580NegativeLiterals.html#556" class="Datatype">Int</a>
    36. 

  36. <a id="803" href="Issue4580NegativeLiterals.html#787" class="Function">minusFive</a> <a id="813" class="Symbol">=</a> <a id="815" class="Number">-5</a>
    37. 

  37. 

  38. <a id="thm"></a><a id="819" href="Issue4580NegativeLiterals.html#819" class="Function">thm</a> <a id="823" class="Symbol">:</a> <a id="825" class="Number">-5</a> <a id="828" href="Agda.Builtin.Equality.html#124" class="Datatype Operator">≡</a> <a id="830" href="Issue4580NegativeLiterals.html#592" class="InductiveConstructor">neg</a> <a id="834" class="Number">4</a>
    39. 

  39. <a id="836" href="Issue4580NegativeLiterals.html#819" class="Function">thm</a> <a id="840" class="Symbol">=</a> <a id="842" href="Agda.Builtin.Equality.html#181" class="InductiveConstructor">refl</a>
    40. 

  40. </pre></body></html>
    41.