\documentclass{article}
\usepackage{agda}
\begin{document}

\begin{code}%
\>\AgdaKeyword{data} \AgdaDatatype{Nat} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{zero} \AgdaSymbol{:} \AgdaDatatype{Nat}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{suc} \AgdaSymbol{:} \AgdaDatatype{Nat} \AgdaSymbol{→} \AgdaDatatype{Nat}\<%
\\
%
\\
\>\AgdaKeyword{module} \AgdaModule{\_} \AgdaKeyword{where}\<%
\\
%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{pattern} \AgdaInductiveConstructor{two} \<[16]%
\>[16]\AgdaSymbol{=} \AgdaInductiveConstructor{suc} \AgdaSymbol{(}\AgdaInductiveConstructor{suc} \AgdaInductiveConstructor{zero}\AgdaSymbol{)}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaKeyword{pattern} \AgdaInductiveConstructor{three} \AgdaSymbol{=} \AgdaInductiveConstructor{suc} \AgdaInductiveConstructor{two}\<%
\\
%
\\
\>\AgdaKeyword{data} \AgdaDatatype{Bot} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\end{code}

\end{document}