Przemebra/praca-magisterska/agda-tex/Nat-double.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{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{ℕ}\<%
%% \\
%% %
%% \\[\AgdaEmptyExtraSkip]%
\>[0]\AgdaFunction{double}\AgdaSpace{}%
\AgdaSymbol{:}\AgdaSpace{}%
\AgdaDatatype{ℕ}\AgdaSpace{}%
\AgdaSymbol{→}\AgdaSpace{}%
\AgdaDatatype{ℕ}\<%
\\
\>[0]\AgdaFunction{double}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{0\#}\<%
\\
\>[0]\AgdaFunction{double}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaBound{n}\AgdaSymbol{)}\AgdaSpace{}%
\AgdaSymbol{=}\AgdaSpace{}%
\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaInductiveConstructor{suc}\AgdaSpace{}%
\AgdaSymbol{(}\AgdaFunction{double}\AgdaSpace{}%
\AgdaBound{n}\AgdaSymbol{))}\<%
\\
\>[0]\<%
\end{code}