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

Issue982.html 5.1 KB
Historie Surový

12345678910111213141516171819202122232425262728 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>Issue982</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. %\renewcommand{\AgdaIndent}{\;\;}
    9. 

  9. 

  10. </a><a id="98" class="Markup">\begin{code}</a>
    11. 

  11. <a id="111" class="Keyword">record</a> <a id="Sigma"></a><a id="118" href="Issue982.html#118" class="Record">Sigma</a> <a id="124" class="Symbol">(</a><a id="125" href="Issue982.html#125" class="Bound">A</a> <a id="127" class="Symbol">:</a> <a id="129" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="132" class="Symbol">)</a> <a id="134" class="Symbol">(</a><a id="135" href="Issue982.html#135" class="Bound">B</a> <a id="137" class="Symbol">:</a> <a id="139" href="Issue982.html#125" class="Bound">A</a> <a id="141" class="Symbol">→</a> <a id="143" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="146" class="Symbol">)</a> <a id="148" class="Symbol">:</a> <a id="150" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="154" class="Keyword">where</a>
    12. 

  12.   <a id="162" class="Keyword">constructor</a> <a id="_,_"></a><a id="174" href="Issue982.html#174" class="InductiveConstructor Operator">_,_</a>
    13. 

  13.   <a id="180" class="Keyword">field</a>
    14. 

  14.     <a id="Sigma.proj₁"></a><a id="190" href="Issue982.html#190" class="Field">proj₁</a> <a id="196" class="Symbol">:</a> <a id="198" href="Issue982.html#125" class="Bound">A</a>
    15. 

  15.     <a id="Sigma.proj₂"></a><a id="204" href="Issue982.html#204" class="Field">proj₂</a> <a id="210" class="Symbol">:</a> <a id="212" href="Issue982.html#135" class="Bound">B</a> <a id="214" href="Issue982.html#190" class="Field">proj₁</a>
    16. 

  16. 

  17. <a id="221" class="Keyword">open</a> <a id="226" href="Issue982.html#118" class="Module">Sigma</a> <a id="232" class="Keyword">public</a>
    18. 

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

  19. 

  20. </a><a id="251" class="Markup">\begin{code}</a>
    21. 

  21. <a id="uncurry"></a><a id="264" href="Issue982.html#264" class="Function">uncurry</a> <a id="272" class="Symbol">:</a> <a id="274" class="Symbol">{</a><a id="275" href="Issue982.html#275" class="Bound">A</a> <a id="277" class="Symbol">:</a> <a id="279" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="282" class="Symbol">}</a> <a id="284" class="Symbol">{</a><a id="285" href="Issue982.html#285" class="Bound">B</a> <a id="287" class="Symbol">:</a> <a id="289" href="Issue982.html#275" 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="Issue982.html#299" class="Bound">C</a> <a id="301" class="Symbol">:</a> <a id="303" href="Issue982.html#118" class="Record">Sigma</a> <a id="309" href="Issue982.html#275" class="Bound">A</a> <a id="311" href="Issue982.html#285" class="Bound">B</a> <a id="313" class="Symbol">→</a> <a id="315" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="318" class="Symbol">}</a> <a id="320" class="Symbol">→</a>
    22. 

  22.           <a id="332" class="Symbol">((</a><a id="334" href="Issue982.html#334" class="Bound">x</a> <a id="336" class="Symbol">:</a> <a id="338" href="Issue982.html#275" class="Bound">A</a><a id="339" class="Symbol">)</a> <a id="341" class="Symbol">→</a> <a id="343" class="Symbol">(</a><a id="344" href="Issue982.html#344" class="Bound">y</a> <a id="346" class="Symbol">:</a> <a id="348" href="Issue982.html#285" class="Bound">B</a> <a id="350" href="Issue982.html#334" class="Bound">x</a><a id="351" class="Symbol">)</a> <a id="353" class="Symbol">→</a> <a id="355" href="Issue982.html#299" class="Bound">C</a> <a id="357" class="Symbol">(</a><a id="358" href="Issue982.html#334" class="Bound">x</a> <a id="360" href="Issue982.html#174" class="InductiveConstructor Operator">,</a> <a id="362" href="Issue982.html#344" class="Bound">y</a><a id="363" class="Symbol">))</a> <a id="366" class="Symbol">→</a>
    23. 

  23.           <a id="378" class="Symbol">((</a><a id="380" href="Issue982.html#380" class="Bound">p</a> <a id="382" class="Symbol">:</a> <a id="384" href="Issue982.html#118" class="Record">Sigma</a> <a id="390" href="Issue982.html#275" class="Bound">A</a> <a id="392" href="Issue982.html#285" class="Bound">B</a><a id="393" class="Symbol">)</a> <a id="395" class="Symbol">→</a> <a id="397" href="Issue982.html#299" class="Bound">C</a> <a id="399" href="Issue982.html#380" class="Bound">p</a><a id="400" class="Symbol">)</a>
    24. 

  24. <a id="402" href="Issue982.html#264" class="Function">uncurry</a> <a id="410" href="Issue982.html#410" class="Bound">f</a> <a id="412" class="Symbol">(</a><a id="413" href="Issue982.html#413" class="Bound">x</a> <a id="415" href="Issue982.html#174" class="InductiveConstructor Operator">,</a> <a id="417" href="Issue982.html#417" class="Bound">y</a><a id="418" class="Symbol">)</a> <a id="420" class="Symbol">=</a> <a id="422" href="Issue982.html#410" class="Bound">f</a> <a id="424" href="Issue982.html#413" class="Bound">x</a> <a id="426" href="Issue982.html#417" class="Bound">y</a>
    25. 

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

  26. 

  27. \end{document}
    28. 

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