caryoscelus
/
agda


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

\usepackage{agda}

\begin{document}

Lemma~\ref{code:B} below shows that $\AgdaPrimitiveType{Set1}$ is inhabited.
%
A preliminary definition:
%
</a><a id="177" class="Markup">\begin{code}[number]</a>
  <a id="A"></a><a id="200" href="Number.html#200" class="Function">A</a> <a id="202" class="Symbol">:</a> <a id="204" href="Agda.Primitive.html#311" class="Primitive">Set1</a>
  <a id="211" href="Number.html#200" class="Function">A</a> <a id="213" class="Symbol">=</a> <a id="215" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="219" class="Markup">\end{code}</a><a id="229" class="Background">
%
Lemma~\ref{code:B2}:
%
</a><a id="255" class="Markup">\begin{code}[number=code:B,number=code:B2]</a>
  <a id="B"></a><a id="300" href="Number.html#300" class="Function">B</a> <a id="302" class="Symbol">:</a> <a id="304" href="Agda.Primitive.html#311" class="Primitive">Set1</a>
  <a id="311" href="Number.html#300" class="Function">B</a> <a id="313" class="Symbol">=</a> <a id="315" href="Number.html#200" class="Function">A</a>
<a id="317" class="Markup">\end{code}</a><a id="327" class="Background">

</a><a id="329" class="Markup">\begin{code}[hide,number=code:Invisible]</a>
  <a id="Invisible"></a><a id="372" href="Number.html#372" class="Function">Invisible</a> <a id="382" class="Symbol">:</a> <a id="384" href="Agda.Primitive.html#311" class="Primitive">Set1</a>
  <a id="391" href="Number.html#372" class="Function">Invisible</a> <a id="401" class="Symbol">=</a> <a id="403" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="407" class="Markup">\end{code}</a><a id="417" class="Background">

Numbers are not generated for inline code, like
%
</a><a id="469" class="Markup">\begin{code}[inline*,number=code:Inline1]</a>
  <a id="Inline1"></a><a id="513" href="Number.html#513" class="Function">Inline1</a> <a id="521" class="Symbol">=</a> <a id="523" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="527" class="Markup">\end{code}</a><a id="537" class="Background">
%
and
%
</a><a id="546" class="Markup">\begin{code}[inline,number=code:Inline2]</a>
  <a id="Inline2"></a><a id="589" href="Number.html#589" class="Function">Inline2</a> <a id="597" class="Symbol">=</a> <a id="599" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="603" class="Markup">\end{code}</a><a id="613" class="Background">.

A wide piece of code:
%
</a><a id="640" class="Markup">\begin{code}[number]</a>
  <a id="Aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"></a><a id="663" href="Number.html#663" class="Function">Aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa</a> <a id="721" class="Symbol">=</a> <a id="723" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="727" class="Markup">\end{code}</a><a id="737" class="Background">

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