caryoscelus
/
agda


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

\usepackage{agda}

\begin{document}

</a><a id="63" class="Markup">\begin{code}</a>
<a id="76" class="Keyword">postulate</a>
  <a id="A"></a><a id="88" href="Relative-indentation.html#88" class="Postulate">A</a>  <a id="B"></a><a id="91" href="Relative-indentation.html#91" class="Postulate">B</a>
      <a id="C"></a><a id="99" href="Relative-indentation.html#99" class="Postulate">C</a> <a id="101" class="Symbol">:</a> <a id="103" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="107" class="Markup">\end{code}</a><a id="117" class="Background">

</a><a id="119" class="Markup">\begin{code}</a>
<a id="132" class="Keyword">postulate</a>
  <a id="D"></a><a id="144" href="Relative-indentation.html#144" class="Postulate">D</a>  <a id="E"></a><a id="147" href="Relative-indentation.html#147" class="Postulate">E</a>

      <a id="F"></a><a id="156" href="Relative-indentation.html#156" class="Postulate">F</a> <a id="158" class="Symbol">:</a> <a id="160" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="164" class="Markup">\end{code}</a><a id="174" class="Background">

</a><a id="176" class="Markup">\begin{code}</a>
<a id="189" class="Keyword">postulate</a>
  <a id="G"></a><a id="201" href="Relative-indentation.html#201" class="Postulate">G</a>  <a id="H"></a><a id="204" href="Relative-indentation.html#204" class="Postulate">H</a>  <a id="207" class="Symbol">:</a> <a id="209" href="Agda.Primitive.html#311" class="Primitive">Set</a>
  <a id="I"></a><a id="215" href="Relative-indentation.html#215" class="Postulate">I</a>
      <a id="J"></a><a id="223" href="Relative-indentation.html#223" class="Postulate">J</a> <a id="225" class="Symbol">:</a> <a id="227" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="231" class="Markup">\end{code}</a><a id="241" class="Background">

\begin{AgdaMultiCode}
</a><a id="265" class="Markup">\begin{code}</a>
<a id="278" class="Keyword">postulate</a>
  <a id="K"></a><a id="290" href="Relative-indentation.html#290" class="Postulate">K</a>  <a id="L"></a><a id="293" href="Relative-indentation.html#293" class="Postulate">L</a>
<a id="295" class="Markup">\end{code}</a><a id="305" class="Background">
</a><a id="306" class="Markup">\begin{code}</a>
      <a id="M"></a><a id="325" href="Relative-indentation.html#325" class="Postulate">M</a> <a id="327" class="Symbol">:</a> <a id="329" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="333" class="Markup">\end{code}</a><a id="343" class="Background">
\end{AgdaMultiCode}

</a><a id="365" class="Markup">\begin{code}</a>
<a id="378" class="Keyword">record</a> <a id="R"></a><a id="385" href="Relative-indentation.html#385" class="Record">R</a> <a id="387" class="Symbol">:</a> <a id="389" href="Agda.Primitive.html#311" class="Primitive">Set₁</a> <a id="394" class="Keyword">where</a>
  <a id="402" class="Keyword">field</a> <a id="R.N"></a><a id="408" href="Relative-indentation.html#408" class="Field">N</a> <a id="410" class="Symbol">:</a>
            <a id="424" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="428" class="Markup">\end{code}</a><a id="438" class="Background">

% There is (and should be) trailing whitespace at the end of some
% lines below.

\begin{AgdaAlign}
text </a><a id="545" class="Markup">\begin{code}        </a>
<a id="566" class="Keyword">module</a> <a id="573" href="Relative-indentation.html#573" class="Module">_</a> <a id="575" class="Keyword">where</a>
<a id="581" class="Markup">\end{code}</a><a id="591" class="Background"> more text
    also text  </a><a id="617" class="Markup">\begin{code}</a>
    <a id="634" class="Keyword">postulate</a> <a id="644" href="Relative-indentation.html#644" class="Postulate">O</a> <a id="646" class="Symbol">:</a> <a id="648" href="Agda.Primitive.html#311" class="Primitive">Set</a>  
  <a id="656" class="Markup">\end{code}</a><a id="666" class="Background"> text again

 text          </a><a id="694" class="Markup">\begin{code}            </a>
    <a id="723" class="Keyword">postulate</a> <a id="733" href="Relative-indentation.html#733" class="Postulate">o</a> <a id="735" class="Symbol">:</a> <a id="737" href="Relative-indentation.html#644" class="Postulate">O</a>    
  <a id="745" class="Markup">\end{code}</a><a id="755" class="Background">   text             
\end{AgdaAlign}

</a><a id="793" class="Markup">\begin{code}</a>
<a id="806" class="Keyword">postulate</a>
 <a id="P"></a><a id="817" href="Relative-indentation.html#817" class="Postulate">P</a> <a id="819" class="Symbol">:</a> <a id="821" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="825" class="Markup">\end{code}</a><a id="835" class="Background">

</a><a id="837" class="Markup">\begin{code}</a>
<a id="850" class="Keyword">module</a> <a id="857" href="Relative-indentation.html#857" class="Module">_</a> <a id="859" class="Keyword">where</a>
 <a id="866" class="Keyword">postulate</a>
  <a id="878" href="Relative-indentation.html#878" class="Postulate">Q</a> <a id="880" class="Symbol">:</a> <a id="882" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="886" class="Markup">\end{code}</a><a id="896" class="Background">

</a><a id="898" class="Markup">\begin{code}</a>
<a id="911" class="Keyword">module</a> <a id="918" href="Relative-indentation.html#918" class="Module">_</a> <a id="920" class="Keyword">where</a>
         <a id="935" class="Keyword">postulate</a>
          <a id="955" href="Relative-indentation.html#955" class="Postulate">S</a> <a id="957" class="Symbol">:</a> <a id="959" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="963" class="Markup">\end{code}</a><a id="973" class="Background">

\begin{AgdaMultiCode}
</a><a id="997" class="Markup">\begin{code}</a>
<a id="1010" class="Keyword">module</a> <a id="1017" href="Relative-indentation.html#1017" class="Module">_</a> <a id="1019" class="Keyword">where</a>
<a id="1025" class="Markup">\end{code}</a><a id="1035" class="Background">
</a><a id="1036" class="Markup">\begin{code}</a>
  <a id="1051" class="Keyword">postulate</a> <a id="1061" href="Relative-indentation.html#1061" class="Postulate">T</a> <a id="1063" class="Symbol">:</a> <a id="1065" href="Agda.Primitive.html#311" class="Primitive">Set</a>
            <a id="1081" href="Relative-indentation.html#1081" class="Postulate">U</a> <a id="1083" class="Symbol">:</a> <a id="1085" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1089" class="Markup">\end{code}</a><a id="1099" class="Background">
\end{AgdaMultiCode}

\begin{AgdaSuppressSpace}
</a><a id="1147" class="Markup">\begin{code}</a>
<a id="1160" class="Keyword">module</a> <a id="1167" href="Relative-indentation.html#1167" class="Module">_</a> <a id="1169" class="Keyword">where</a>
<a id="1175" class="Markup">\end{code}</a><a id="1185" class="Background">
</a><a id="1186" class="Markup">\begin{code}</a>
  <a id="1201" class="Keyword">postulate</a> <a id="1211" href="Relative-indentation.html#1211" class="Postulate">V</a> <a id="1213" class="Symbol">:</a> <a id="1215" href="Agda.Primitive.html#311" class="Primitive">Set</a>
            <a id="1231" href="Relative-indentation.html#1231" class="Postulate">W</a> <a id="1233" class="Symbol">:</a> <a id="1235" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1239" class="Markup">\end{code}</a><a id="1249" class="Background">
\end{AgdaSuppressSpace}

</a><a id="1275" class="Markup">\begin{code}</a>
<a id="X"></a><a id="1288" href="Relative-indentation.html#1288" class="Function">X</a> <a id="1290" class="Symbol">:</a> <a id="1292" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
<a id="1297" href="Relative-indentation.html#1288" class="Function">X</a> <a id="1299" class="Symbol">=</a>
  <a id="1303" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1307" class="Markup">\end{code}</a><a id="1317" class="Background">

</a><a id="1319" class="Markup">\begin{code}</a>
<a id="Y"></a><a id="1332" href="Relative-indentation.html#1332" class="Function">Y</a> <a id="1334" class="Symbol">:</a> <a id="1336" href="Agda.Primitive.html#311" class="Primitive">Set₁</a>
<a id="1341" href="Relative-indentation.html#1332" class="Function">Y</a> <a id="1343" class="Symbol">=</a>       <a id="1351" href="Agda.Primitive.html#311" class="Primitive">Set</a>

<a id="Zzzzzzzzz"></a><a id="1356" href="Relative-indentation.html#1356" class="Function">Zzzzzzzzz</a> <a id="1366" class="Symbol">:</a> <a id="1368" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="1372" class="Symbol">→</a> <a id="1374" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="1378" href="Relative-indentation.html#1356" class="Function">Zzzzzzzzz</a> <a id="1388" href="Relative-indentation.html#1388" class="Bound">X</a>
          <a id="1400" class="Symbol">=</a> <a id="1402" href="Relative-indentation.html#1388" class="Bound">X</a>
<a id="1404" class="Markup">\end{code}</a><a id="1414" class="Background">

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