--- a/paper/tex/agda.tex	Thu Feb 11 23:36:12 2021 +0900
+++ b/paper/tex/agda.tex	Fri Feb 12 18:02:24 2021 +0900
@@ -9,10 +9,10 @@
 は記述したプログラムを証明することができる。
 
 \section{Agdaの基本}
+本節ではAgdaの基本事項についてソースコードを例に出しながら説明を行う。
 
 \subsection{関数の実装}
-本節ではAgdaの基本事項について \coderef{plus} を例として解説する。
-
+Agdaでの関数の 定義方法について \coderef{plus} を例として解説する。
 基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。
 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
 ここでは関数を実行した際の例を記述している。
@@ -24,10 +24,10 @@
 この : の前が関数名になり、その後ろがその関数の定義となる。
 : 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。
 $ \rightarrow $ 以降は関数が返す型を記述している。
-まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
+まとめると、この関数 plus は、型が自然数である2つの変数 x, y を受け取り、
 自然数を返すという定義になる。
 
-関数の定義をしたコードの直下で実装を行うのが常である。
+Agda では関数の定義をしたコードの直下で実装を行うのが常である。
 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
 引数に対応した実装をする。
 
@@ -51,15 +51,17 @@
 利点としては、直感的な記号論理の記述ができる。
 以下、記号論理は基本的に三項演算子を使用して記述する。
 
+\begin{comment}
 \subsection{Agdaにおけるラムダ計算}
 \lambda
+\end{comment}
 
 \subsection{Data 型の実装}
 Deta 型とは分岐のことである。
 そのため、それぞれの動作について実装する必要がある。
-例として既出で Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。
+例として既出の Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。
 
-\lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda}
+\lstinputlisting[label=Nat, caption=Natural の定義] {src/agda/Nat.agda}
 
 実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
 それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、
@@ -72,13 +74,13 @@
 言い換えればパターンマッチをする必要があると言える。
 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。
 
-\subsection{パターンマッチ}
+% \subsection{パターンマッチ}
 
 \subsection{Record 型の実装}
 Record 型とはオブジェクトあるいは構造体ののようなものである。
 \coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。
 
-\lstinputlisting[label=And, caption=And] {src/agda/And.agda}
+\lstinputlisting[label=And の定義, caption=And] {src/agda/And.agda}
 
 また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。
 
@@ -86,7 +88,7 @@
 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
 \coderef{syllogism}を以下に示す。
 
-\lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda}
+\lstinputlisting[label=syllogism の実装, caption=syllogism] {src/agda/syllogism.agda}
 
 コードの解説をすると、引数として x と a が関数に与えられている。
 引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身
@@ -94,7 +96,9 @@
 \_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。
 よって A を与えて C を取得することができたため、三段論法を定義できた。
 
-\section{Agdaで使用するもの}
+\section{本論で使用する Agda の記法}
+本論では、ソースコードを出しながら実施内容について述べるが、
+特殊な記法を用いている場合があるので、前もって解説をする。
 
 \subsection{Agdaの省略記法}
 Recode が入力された場合のことを考える。この際、入力時に record を展開してしまうと、