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
/
Issue2744.html

Issue2744.html 4.5 KB
Historie Surový

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>Issue2744</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. \noindent Before.
    9. 

  9. \begin{AgdaMultiCode}
    10. 

  10. </a><a id="103" class="Markup">\begin{code}[hide]</a>
    11. 

  11.   <a id="124" class="Keyword">postulate</a>
    12. 

  12. <a id="134" class="Markup">\end{code}</a><a id="144" class="Background">
    13. 

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

  14.     <a id="A"></a><a id="162" href="Issue2744.html#162" class="Postulate">A</a>    <a id="167" class="Symbol">:</a> <a id="169" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    15. 

  15. <a id="173" class="Markup">\end{code}</a><a id="183" class="Background">
    16. 

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

  17.     <a id="BBB"></a><a id="201" href="Issue2744.html#201" class="Postulate">BBB</a>  <a id="206" class="Symbol">:</a> <a id="208" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    18. 

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

  19. \end{AgdaMultiCode}
    20. 

  20. After.
    21. 

  21. 

  22. \noindent Before.
    23. 

  23. \begin{AgdaAlign}
    24. 

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

  25.   <a id="302" class="Keyword">postulate</a>
    26. 

  26.     <a id="C"></a><a id="316" href="Issue2744.html#316" class="Postulate">C</a> <a id="318" class="Symbol">:</a> <a id="320" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    27. 

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

  28. </a><a id="335" class="Markup">\begin{code}[hide]</a>
    29. 

  29.     <a id="D"></a><a id="358" href="Issue2744.html#358" class="Postulate">D</a> <a id="360" class="Symbol">:</a> <a id="362" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    30. 

  30. <a id="366" class="Markup">\end{code}</a><a id="376" class="Background">
    31. 

  31. </a><a id="377" class="Markup">\begin{code}</a>
    32. 

  32.     <a id="E"></a><a id="394" href="Issue2744.html#394" class="Postulate">E</a> <a id="396" class="Symbol">:</a> <a id="398" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    33. 

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

  34. \end{AgdaAlign}
    35. 

  35. After.
    36. 

  36. 

  37. \noindent Before.
    38. 

  38. \begin{AgdaAlign}
    39. 

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

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

  41.     <a id="F"></a><a id="502" href="Issue2744.html#502" class="Postulate">F</a> <a id="504" class="Symbol">:</a> <a id="506" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    42. 

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

  43. In between.
    44. 

  44. \begin{AgdaSuppressSpace}
    45. 

  45. </a><a id="559" class="Markup">\begin{code}</a>
    46. 

  46.   <a id="574" class="Keyword">postulate</a>
    47. 

  47.     <a id="G"></a><a id="588" href="Issue2744.html#588" class="Postulate">G</a> <a id="590" class="Symbol">:</a> <a id="592" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    48. 

  48. <a id="596" class="Markup">\end{code}</a><a id="606" class="Background">
    49. 

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

  50.   <a id="628" class="Keyword">postulate</a>
    51. 

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

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

  53.     <a id="H"></a><a id="666" href="Issue2744.html#666" class="Postulate">H</a> <a id="668" class="Symbol">:</a> <a id="670" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    54. 

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

  55. \end{AgdaSuppressSpace}
    56. 

  56. \end{AgdaAlign}
    57. 

  57. After.
    58. 

  58. 

  59. \noindent Before.
    60. 

  60. \begin{AgdaMultiCode}
    61. 

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

  62.   <a id="788" class="Keyword">postulate</a>
    63. 

  63.     <a id="!_!"></a><a id="802" href="Issue2744.html#802" class="Postulate Operator">!_!</a>    <a id="809" class="Symbol">:</a> <a id="811" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="815" class="Symbol">→</a> <a id="817" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    64. 

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

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

  66.   <a id="853" class="Keyword">postulate</a>
    67. 

  67. <a id="863" class="Markup">\end{code}</a><a id="873" class="Background">
    68. 

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

  69.     <a id="&lt;!_!&gt;"></a><a id="891" href="Issue2744.html#891" class="Postulate Operator">&lt;!_!&gt;</a>  <a id="898" class="Symbol">:</a> <a id="900" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="904" class="Symbol">→</a> <a id="906" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    70. 

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

  71. \end{AgdaMultiCode}
    72. 

  72. After.
    73. 

  73. 

  74. \end{document}
    75. 

  75. </a></pre></body></html>
    76.