Mercurial > hg > Papers > 2020 > ryokka-master
changeset 3:a6f371a5d33d
fix
| author | ryokka |
|---|---|
| date | Mon, 27 Jan 2020 20:46:38 +0900 |
| parents | c7acb9211784 |
| children | b5fffa8ae875 |
| files | paper/cbc_agda.tex paper/master_paper.pdf |
| diffstat | 2 files changed, 7 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- 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 を定義している。