--- a/tex/agda.tex	Mon Sep 14 05:41:23 2020 +0900
+++ b/tex/agda.tex	Mon Sep 14 19:58:10 2020 +0900
@@ -7,8 +7,7 @@
 
 \subsection{プログラムの読み方}
 以下は Agda プログラムの一例となる。
-本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、
-後述する Agda コードの理解を容易にすることを目的としている。
+本節ではAgdaの基本事項について解説する。
 
 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
@@ -24,7 +23,6 @@
 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
 自然数を返すという定義になる。
 		
-実装部分の説明をする。
 関数の定義をしたコードの直下で実装を行うのが常である。
 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
 引数に対応した実装をする。
@@ -36,7 +34,7 @@
 
 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
 y が 0 になった際に計算が終了となっている。
-指折りでの足し算を実装していると捉えても良い
+指折りでの足し算を実装していると捉えても良い。
 
 \subsection{Data 型}
 Deta 型とは分岐のことである。