caryoscelus
/
agda


			
				
					
						
						
							1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859
							<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Trailing-whitespace</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}
\AgdaNoSpaceAroundCode{}

\begin{document}

\hrule
</a><a id="95" class="Markup">\begin{code}</a>
<a id="108" class="Keyword">postulate</a>
  
  <a id="A"></a><a id="123" href="Trailing-whitespace.html#123" class="Postulate">A</a> <a id="125" class="Symbol">:</a> <a id="127" href="Agda.Primitive.html#311" class="Primitive">Set</a>  
  <a id="B"></a><a id="135" href="Trailing-whitespace.html#135" class="Postulate">B</a> <a id="137" class="Symbol">:</a> <a id="139" href="Agda.Primitive.html#311" class="Primitive">Set</a>  
<a id="145" class="Markup">\end{code}</a><a id="155" class="Background">
\hrule
</a><a id="163" class="Markup">\begin{code}</a>
  
<a id="179" class="Markup">\end{code}</a><a id="189" class="Background">
\hrule
</a><a id="197" class="Markup">\begin{code}</a>

<a id="211" class="Markup">\end{code}</a><a id="221" class="Background">
\hrule
</a><a id="229" class="Markup">\begin{code}</a>
<a id="242" class="Markup">\end{code}</a><a id="252" class="Background">
\hrule
</a><a id="260" class="Markup">\begin{code}  </a>
  <a id="277" class="Markup">\end{code}</a><a id="287" class="Background">
\hrule
  </a><a id="297" class="Markup">\begin{code}  </a>
<a id="312" class="Markup">\end{code}</a><a id="322" class="Background">
\hrule
  </a><a id="332" class="Markup">\begin{code}  </a>
    <a id="351" class="Markup">\end{code}</a><a id="361" class="Background">
\hrule
</a><a id="369" class="Markup">\begin{code}</a>
<a id="382" class="Keyword">module</a> <a id="389" href="Trailing-whitespace.html#389" class="Module">_</a> <a id="391" class="Keyword">where</a>
<a id="397" class="Markup">\end{code}</a><a id="407" class="Background">
</a><a id="408" class="Markup">\begin{code}</a>
  
  <a id="426" class="Keyword">postulate</a>
    <a id="440" href="Trailing-whitespace.html#440" class="Postulate">C</a> <a id="442" class="Symbol">:</a> <a id="444" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="448" class="Markup">\end{code}</a><a id="458" class="Background">
\hrule
\begin{AgdaAlign}
</a><a id="484" class="Markup">\begin{code}</a>
<a id="497" class="Keyword">postulate</a>
  <a id="F"></a><a id="509" href="Trailing-whitespace.html#509" class="Postulate">F</a>  <a id="512" class="Symbol">:</a> <a id="514" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="518" class="Symbol">→</a> <a id="520" href="Agda.Primitive.html#311" class="Primitive">Set</a>
  <a id="X"></a><a id="526" href="Trailing-whitespace.html#526" class="Postulate">X</a>  <a id="529" class="Symbol">:</a> <a id="531" href="Trailing-whitespace.html#509" class="Postulate">F</a>  
<a id="535" class="Markup">\end{code}</a><a id="545" class="Background">
</a><a id="546" class="Markup">\begin{code}</a>
          <a id="569" href="Trailing-whitespace.html#123" class="Postulate">A</a>
<a id="571" class="Markup">\end{code}</a><a id="581" class="Background">
\end{AgdaAlign}
\hrule

\end{document}
</a></pre></body></html>