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

QuickLaTeX.html 4.0 KB
History Raw

12345678910111213141516171819202122232425262728 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>QuickLaTeX</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. </a><a id="63" class="Markup">\begin{code}</a>
    9. 

  9. <a id="76" class="Symbol">{-#</a> <a id="80" class="Keyword">OPTIONS</a> <a id="88" class="Pragma">--sized-types</a> <a id="102" class="Symbol">#-}</a>
    10. 

  10. 

  11. <a id="107" class="Symbol">{-#</a> <a id="111" class="Keyword">BUILTIN</a> <a id="119" class="Keyword">SIZE</a> <a id="Size"></a><a id="124" href="QuickLaTeX.html#124" class="Postulate">Size</a> <a id="129" class="Symbol">#-}</a>
    12. 

  12. 

  13. <a id="134" class="Keyword">record</a> <a id="Sigma"></a><a id="141" href="QuickLaTeX.html#141" class="Record">Sigma</a> <a id="147" class="Symbol">(</a><a id="148" href="QuickLaTeX.html#148" class="Bound">A</a> <a id="150" class="Symbol">:</a> <a id="152" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="155" class="Symbol">)</a> <a id="157" class="Symbol">(</a><a id="158" href="QuickLaTeX.html#158" class="Bound">B</a> <a id="160" class="Symbol">:</a> <a id="162" href="QuickLaTeX.html#148" class="Bound">A</a> <a id="164" class="Symbol">→</a> <a id="166" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="169" class="Symbol">)</a> <a id="171" class="Symbol">:</a> <a id="173" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="177" class="Keyword">where</a>
    14. 

  14.   <a id="185" class="Keyword">coinductive</a>
    15. 

  15.   <a id="199" class="Keyword">constructor</a> <a id="c"></a><a id="211" href="QuickLaTeX.html#211" class="CoinductiveConstructor">c</a>
    16. 

  16.   <a id="215" class="Keyword">field</a>
    17. 

  17.     <a id="Sigma.proj₁"></a><a id="225" href="QuickLaTeX.html#225" class="Field">proj₁</a> <a id="231" class="Symbol">:</a> <a id="233" href="QuickLaTeX.html#148" class="Bound">A</a>
    18. 

  18.     <a id="Sigma.proj₂"></a><a id="239" href="QuickLaTeX.html#239" class="Field">proj₂</a> <a id="245" class="Symbol">:</a> <a id="247" href="QuickLaTeX.html#158" class="Bound">B</a> <a id="249" href="QuickLaTeX.html#225" class="Field">proj₁</a>
    19. 

  19. 

  20. <a id="256" class="Keyword">data</a> <a id="D"></a><a id="261" href="QuickLaTeX.html#261" class="Datatype">D</a> <a id="263" class="Symbol">:</a> <a id="265" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="269" class="Keyword">where</a>
    21. 

  21.   <a id="D.c"></a><a id="277" href="QuickLaTeX.html#277" class="InductiveConstructor">c</a> <a id="279" class="Symbol">:</a> <a id="281" href="QuickLaTeX.html#261" class="Datatype">D</a>
    22. 

  22. 

  23. <a id="f"></a><a id="284" href="QuickLaTeX.html#284" class="Function">f</a> <a id="286" class="Symbol">:</a> <a id="288" class="Symbol">{</a><a id="289" href="QuickLaTeX.html#289" class="Bound">A</a> <a id="291" class="Symbol">:</a> <a id="293" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="296" class="Symbol">}</a> <a id="298" class="Symbol">{</a><a id="299" href="QuickLaTeX.html#299" class="Bound">B</a> <a id="301" class="Symbol">:</a> <a id="303" href="QuickLaTeX.html#289" class="Bound">A</a> <a id="305" class="Symbol">→</a> <a id="307" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="310" class="Symbol">}</a> <a id="312" class="Symbol">(</a><a id="313" href="QuickLaTeX.html#313" class="Bound">x</a> <a id="315" class="Symbol">:</a> <a id="317" href="QuickLaTeX.html#289" class="Bound">A</a><a id="318" class="Symbol">)</a> <a id="320" class="Symbol">→</a> <a id="322" href="QuickLaTeX.html#299" class="Bound">B</a> <a id="324" href="QuickLaTeX.html#313" class="Bound">x</a> <a id="326" class="Symbol">→</a> <a id="328" href="QuickLaTeX.html#141" class="Record">Sigma</a> <a id="334" href="QuickLaTeX.html#289" class="Bound">A</a> <a id="336" href="QuickLaTeX.html#299" class="Bound">B</a>
    24. 

  24. <a id="338" href="QuickLaTeX.html#284" class="Function">f</a> <a id="340" class="Symbol">=</a> <a id="342" href="QuickLaTeX.html#211" class="CoinductiveConstructor">c</a>
    25. 

  25. <a id="344" class="Markup">\end{code}</a><a id="354" class="Background">
    26. 

  26. 

  27. \end{document}
    28. 

  28. </a></pre></body></html>
    29.