| 123456789101112131415161718192021222324252627282930313233 |
- <!DOCTYPE HTML>
- <html><head><meta charset="utf-8"><title>Inline</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}
- \usepackage{agda}
- \begin{document}
- Assume that we are given a type
- %
- </a><a id="97" class="Markup">\begin{code}[inline=False,hide=true]</a>
- <a id="136" class="Keyword">module</a> <a id="143" href="Inline.html" class="Module">_</a> <a id="145" class="Symbol">(</a>
- <a id="147" class="Markup">\end{code}</a><a id="157" class="Background">
- </a><a id="158" class="Markup">\begin{code}[hide,inline,hide=false]</a>
- <a id="199" href="Inline.html#199" class="Bound">A</a> <a id="201" class="Symbol">:</a> <a id="203" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="207" class="Markup">\end{code}</a><a id="217" class="Background">
- </a><a id="218" class="Markup">\begin{code}[hide=false,hide=True]</a>
- <a id="257" class="Symbol">)</a> <a id="259" class="Symbol">(</a>
- <a id="261" class="Markup">\end{code}</a><a id="271" class="Background">
- %
- ,
- and that a function
- %
- </a><a id="298" class="Markup">\begin{code}[inline*]</a>
- <a id="324" href="Inline.html#324" class="Bound">F</a> <a id="326" class="Symbol">:</a> <a id="328" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="332" class="Symbol">→</a> <a id="334" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="338" class="Symbol">→</a> <a id="340" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="344" class="Symbol">→</a> <a id="346" href="Agda.Primitive.html#311" class="Primitive">Set</a>
- <a id="350" class="Markup">\end{code}</a><a id="360" class="Background">
- </a><a id="361" class="Markup">\begin{code}[hide]</a>
- <a id="384" class="Symbol">)</a> <a id="386" class="Keyword">where</a>
- <a id="392" class="Markup">\end{code}</a><a id="402" class="Background">
- %
- is also given.
- \end{document}
- </a></pre></body></html>
|
