\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{code}%
\>\AgdaKeyword{data} \AgdaDatatype{Nat} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaKeyword{where}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{zero} \<[8]%
\>[8]\AgdaSymbol{:} \AgdaDatatype{Nat}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaInductiveConstructor{suc} \<[8]%
\>[8]\AgdaSymbol{:} \AgdaDatatype{Nat} \AgdaSymbol{->} \AgdaDatatype{Nat}\<%
\end{code}

\end{document}
