# HG changeset patch
# User ryokka
# Date 1580125598 -32400
# Node ID a6f371a5d33de2599ce8867d67759271c7bb8d20
# Parent  c7acb9211784352d3e1aaa70c22191c1a4073b84
fix

diff -r c7acb9211784 -r a6f371a5d33d paper/cbc_agda.tex
--- a/paper/cbc_agda.tex	Mon Jan 27 20:41:36 2020 +0900
+++ b/paper/cbc_agda.tex	Mon Jan 27 20:46:38 2020 +0900
@@ -18,16 +18,16 @@
 次の CodeGear へ継続を行う。
 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当するため、
 継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。
-継続は不定の型 (\verb+t+) を返す関数で表される。
-CodeGear は次に実行する関数の型を引数として受け取り不定の型\verb+t+を返す関数として記述され、
-CodeGear 自体も同じ型 \verb+t+ を返す関数となる。
+継続は不定の型 (\verb/t/) を返す関数で表される。
+CodeGear は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、
+CodeGear 自体も同じ型 \verb/t/ を返す関数となる。
 コード \ref{agda-cg} は Agda で記述した CodeGear の例である。
 
-\lstinputlisting[caption= whileTest の型,label=agda-cg]{src/while-test.agda.replaced}
+\lstinputlisting[caption= whileTest の型, label=agda-cg]{src/while-test.agda.replaced}
 %% Agda のとこで Level の話を…！
-ここでは \verb+c10+ と名付けた自然数を受け取った後、
-\varb+Env+ を受け取って不定の型\verb+t+を返す関数を受け取り、
-\verb+t+を返す CodeGear を定義している。
+ここでは \verb/c10/ と名付けた自然数を受け取った後、
+\verb/Env/ を受け取って不定の型\verb/t/を返す関数を受け取り、
+\verb/t/を返す CodeGear を定義している。
 
 
 
diff -r c7acb9211784 -r a6f371a5d33d paper/master_paper.pdf
Binary file paper/master_paper.pdf has changed