agda/test/LaTeXAndHTML/succeed/Number.tex

\documentclass[draft]{article}

\usepackage{agda}

\begin{document}

Lemma~\ref{code:B} below shows that $\AgdaPrimitiveType{Set1}$ is inhabited.
%
A preliminary definition:
%
\begin{code}[number]%
%
\>[2]\AgdaFunction{A}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set1}\<%
\\
%
\>[2]\AgdaFunction{A}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
%
Lemma~\ref{code:B2}:
%
\begin{code}[number=code:B,number=code:B2]%
%
\>[2]\AgdaFunction{B}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set1}\<%
\\
%
\>[2]\AgdaFunction{B}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaFunction{A}\<%
\end{code}

\begin{code}[hide,number=code:Invisible]%
%
\>[2]\AgdaFunction{Invisible}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitive{Set1}\<%
\\
%
\>[2]\AgdaFunction{Invisible}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

Numbers are not generated for inline code, like
%
\begin{code}[inline*,number=code:Inline1]%
%
\>[2]\AgdaFunction{Inline1}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}
%
and
%
\begin{code}[inline,number=code:Inline2]%
%
\>[2]\AgdaFunction{Inline2}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}.

A wide piece of code:
%
\begin{code}[number]%
%
\>[2]\AgdaFunction{Aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaPrimitive{Set}\<%
\end{code}

\end{document}