Przemebra/praca-magisterska/agda-tex/Nat.tex

\begin{code}%
%\>[0]\<%
%\\
%% \>[0]\AgdaKeyword{open}\AgdaSpace{}%
%% \AgdaKeyword{import}\AgdaSpace{}%
%% \AgdaModule{Level}\AgdaSpace{}%
%% \AgdaKeyword{using}\AgdaSpace{}%
%% \AgdaSymbol{(}\AgdaPrimitive{zero}\AgdaSymbol{)}\<%
%% \\
%% %
%% \\[\AgdaEmptyExtraSkip]%
%% \>[0]\AgdaKeyword{module}\AgdaSpace{}%
%% \AgdaModule{latex.Nat}\AgdaSpace{}%
%% \AgdaKeyword{where}\<%
%% \\
%% %
%\\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaKeyword{data}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaPrimitiveType{Set}\AgdaSpace{}%
\AgdaPrimitive{zero}\AgdaSpace{}%
\AgdaKeyword{where}\<%
\\
\>[0][@{}l@{\AgdaIndent{0}}]%
\>[2]\AgdaInductiveConstructor{0\#}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
%
\>[2]\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
\>[0]\<%
\end{code}