\chapter{chapter:sources}
本論文中に取り上げた Agda の動作するソースコードを示す。

\section{ノーマルレベル動作の実行}
\label{appendix:normal-level-exec}
\ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。

\lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル実行の完全なソースコード] {src/atton-master-sample.agda}