홈 탐색 도움말
로그인
caryoscelus
/
agda
Watch 1
Star 0
포크 0
파일 이슈 0 풀 리퀘스트 0 위키
트리: ce9b406819
브랜치 태그
agda
/
test
/
LaTeXAndHTML
/
succeed
/
IndentingContainer.html

IndentingContainer.html 6.6 KB
히스토리 Raw

12345678910111213141516171819202122232425262728293031323334 
  1. <!DOCTYPE HTML>
    2. 

  2. <html><head><meta charset="utf-8"><title>IndentingContainer</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="Keyword">record</a> <a id="Sigma"></a><a id="83" href="IndentingContainer.html#83" class="Record">Sigma</a> <a id="89" class="Symbol">(</a><a id="90" href="IndentingContainer.html#90" class="Bound">A</a> <a id="92" class="Symbol">:</a> <a id="94" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="97" class="Symbol">)</a> <a id="99" class="Symbol">(</a><a id="100" href="IndentingContainer.html#100" class="Bound">B</a> <a id="102" class="Symbol">:</a> <a id="104" href="IndentingContainer.html#90" class="Bound">A</a> <a id="106" class="Symbol">→</a> <a id="108" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="111" class="Symbol">)</a> <a id="113" class="Symbol">:</a> <a id="115" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="119" class="Keyword">where</a>
    10. 

  10.   <a id="127" class="Keyword">constructor</a> <a id="_,_"></a><a id="139" href="IndentingContainer.html#139" class="InductiveConstructor Operator">_,_</a>
    11. 

  11.   <a id="145" class="Keyword">field</a>
    12. 

  12.     <a id="Sigma.proj₁"></a><a id="155" href="IndentingContainer.html#155" class="Field">proj₁</a> <a id="161" class="Symbol">:</a> <a id="163" href="IndentingContainer.html#90" class="Bound">A</a>
    13. 

  13.     <a id="Sigma.proj₂"></a><a id="169" href="IndentingContainer.html#169" class="Field">proj₂</a> <a id="175" class="Symbol">:</a> <a id="177" href="IndentingContainer.html#100" class="Bound">B</a> <a id="179" href="IndentingContainer.html#155" class="Field">proj₁</a>
    14. 

  14. 

  15. <a id="186" class="Keyword">open</a> <a id="191" href="IndentingContainer.html#83" class="Module">Sigma</a> <a id="197" class="Keyword">public</a>
    16. 

  16. <a id="204" class="Markup">\end{code}</a><a id="214" class="Background">
    17. 

  17. 

  18. </a><a id="216" class="Markup">\begin{code}</a>
    19. 

  19. <a id="uncurry"></a><a id="229" href="IndentingContainer.html#229" class="Function">uncurry</a> <a id="237" class="Symbol">:</a> <a id="239" class="Symbol">{</a><a id="240" href="IndentingContainer.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="250" href="IndentingContainer.html#250" class="Bound">B</a> <a id="252" class="Symbol">:</a> <a id="254" href="IndentingContainer.html#240" class="Bound">A</a> <a id="256" class="Symbol">→</a> <a id="258" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="261" class="Symbol">}</a> <a id="263" class="Symbol">{</a><a id="264" href="IndentingContainer.html#264" class="Bound">C</a> <a id="266" class="Symbol">:</a> <a id="268" href="IndentingContainer.html#83" class="Record">Sigma</a> <a id="274" href="IndentingContainer.html#240" class="Bound">A</a> <a id="276" href="IndentingContainer.html#250" class="Bound">B</a> <a id="278" class="Symbol">→</a> <a id="280" href="Agda.Primitive.html#311" class="Primitive">Set</a><a id="283" class="Symbol">}</a> <a id="285" class="Symbol">→</a>
    20. 

  20.           <a id="297" class="Symbol">((</a><a id="299" href="IndentingContainer.html#299" class="Bound">x</a> <a id="301" class="Symbol">:</a> <a id="303" href="IndentingContainer.html#240" class="Bound">A</a><a id="304" class="Symbol">)</a> <a id="306" class="Symbol">→</a> <a id="308" class="Symbol">(</a><a id="309" href="IndentingContainer.html#309" class="Bound">y</a> <a id="311" class="Symbol">:</a> <a id="313" href="IndentingContainer.html#250" class="Bound">B</a> <a id="315" href="IndentingContainer.html#299" class="Bound">x</a><a id="316" class="Symbol">)</a> <a id="318" class="Symbol">→</a> <a id="320" href="IndentingContainer.html#264" class="Bound">C</a> <a id="322" class="Symbol">(</a><a id="323" href="IndentingContainer.html#299" class="Bound">x</a> <a id="325" href="IndentingContainer.html#139" class="InductiveConstructor Operator">,</a> <a id="327" href="IndentingContainer.html#309" class="Bound">y</a><a id="328" class="Symbol">))</a> <a id="331" class="Symbol">→</a>
    21. 

  21.           <a id="343" class="Symbol">((</a><a id="345" href="IndentingContainer.html#345" class="Bound">p</a> <a id="347" class="Symbol">:</a> <a id="349" href="IndentingContainer.html#83" class="Record">Sigma</a> <a id="355" href="IndentingContainer.html#240" class="Bound">A</a> <a id="357" href="IndentingContainer.html#250" class="Bound">B</a><a id="358" class="Symbol">)</a> <a id="360" class="Symbol">→</a> <a id="362" href="IndentingContainer.html#264" class="Bound">C</a> <a id="364" href="IndentingContainer.html#345" class="Bound">p</a><a id="365" class="Symbol">)</a>
    22. 

  22. <a id="367" href="IndentingContainer.html#229" class="Function">uncurry</a> <a id="375" href="IndentingContainer.html#375" class="Bound">f</a> <a id="377" class="Symbol">(</a><a id="378" href="IndentingContainer.html#378" class="Bound">x</a> <a id="380" href="IndentingContainer.html#139" class="InductiveConstructor Operator">,</a> <a id="382" href="IndentingContainer.html#382" class="Bound">y</a><a id="383" class="Symbol">)</a> <a id="385" class="Symbol">=</a> <a id="387" href="IndentingContainer.html#375" class="Bound">f</a> <a id="389" href="IndentingContainer.html#378" class="Bound">x</a> <a id="391" href="IndentingContainer.html#382" class="Bound">y</a>
    23. 

  23. <a id="393" class="Markup">\end{code}</a><a id="403" class="Background">
    24. 

  24. 

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

  26. <a id="418" class="Keyword">record</a> <a id="Container"></a><a id="425" href="IndentingContainer.html#425" class="Record">Container</a> <a id="435" class="Symbol">:</a> <a id="437" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="442" class="Keyword">where</a>
    27. 

  27.   <a id="450" class="Keyword">constructor</a> <a id="_◃_"></a><a id="462" href="IndentingContainer.html#462" class="InductiveConstructor Operator">_◃_</a>
    28. 

  28.   <a id="468" class="Keyword">field</a>
    29. 

  29.     <a id="Container.Parameter"></a><a id="478" href="IndentingContainer.html#478" class="Field">Parameter</a> <a id="488" class="Symbol">:</a> <a id="490" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    30. 

  30.     <a id="Container.Arity"></a><a id="498" href="IndentingContainer.html#498" class="Field">Arity</a> <a id="504" class="Symbol">:</a> <a id="506" href="IndentingContainer.html#478" class="Field">Parameter</a> <a id="516" class="Symbol">→</a> <a id="518" href="Agda.Primitive.html#311" class="Primitive">Set</a>
    31. 

  31. <a id="522" class="Markup">\end{code}</a><a id="532" class="Background">
    32. 

  32. 

  33. \end{document}
    34. 

  34. </a></pre></body></html>
    35.