--- a/tex/agda.tex	Mon Sep 14 02:58:14 2020 +0900
+++ b/tex/agda.tex	Mon Sep 14 05:41:23 2020 +0900
@@ -9,43 +9,34 @@
 以下は Agda プログラムの一例となる。
 本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、
 後述する Agda コードの理解を容易にすることを目的としている。
+
+基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
+また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
+ここでは関数を実行した際の例を記述している。
+したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
+
 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda}
 
-\begin{itemize}
-	\item 基本事項
-		\begin{itemize}
-			\item 
-				ℕ というのは自然数 (Natulal Number) のことである。
-				また、- (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
-				ここでは関数を実行した際の例を記述している。
-				したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
-		\end{itemize}
-    \item 定義部分
-		\begin{itemize}
-			\item 
-				コードの1行目に : (セミコロン)がある。
-				この : の前が関数名になり、その後ろがその関数の定義となる。\\
-				: の後ろの (x y : ℕ ) は関数は x, y の自然数2つを受けとる。
-				という意味になる。
-				→ の後ろは関数が返す型を記述している。
-				まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
-				自然数を返すという定義になる。
-		\end{itemize}
-	\item 実装部分
-		\begin{itemize}
-			\item 
-				関数の定義をしたコードの直下で実装を行うのが常である。
-				関数名を記述した後に引数を記述して受け取り、= (イコール) の後ろで
-				引数に対応し実装を作を記述していく。
-				今回の場合では、 plus x zero であれば +0 である為、そのまま x を返す。
-				2行目の方では受け取った y の値を減らし、x の値を増やして再び plus の関数に
-				遷移している。
-				受け取った y は+1されていたことにすることでyの値を減らしている。
-				実装部分もまとめると、x と y の値を足す為に、y から x に数値を1つずつ渡す。
-				y が 0 になった際に計算が終了となっている。
-				指折りでの足し算を実装していると捉えても良い
-		\end{itemize}
-\end{itemize}
+この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。
+この : の前が関数名になり、その後ろがその関数の定義となる。
+: 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。
+→ 以降は関数が返す型を記述している。
+まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
+自然数を返すという定義になる。
+		
+実装部分の説明をする。
+関数の定義をしたコードの直下で実装を行うのが常である。
+関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
+引数に対応した実装をする。
+
+今回の場合 plus x zero であれば +0 である為、そのまま x を返す。
+実装2行目の方で受け取った y の値を減らし、x の値を増やして再び plus の関数に
+遷移している。
+受け取った y を +1 されていたとして y の値を減らしている。
+
+関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
+y が 0 になった際に計算が終了となっている。
+指折りでの足し算を実装していると捉えても良い
 
 \subsection{Data 型}
 Deta 型とは分岐のことである。