Mercurial > hg > Papers > 2021 > soto-thesis

annotate paper/tex/continuation_agda.tex @ 3:959f4b34d6f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final thesis
author soto
date Tue, 09 Feb 2021 18:44:53 +0900
parents
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
1 \section{Code Gearに合わせた Agda}
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
2 検証を行うために、AgdaのコードもCbCに合わせて記述を行う必要がある。
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
3 実際に以下がコードとなる。
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
4
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
5 CbCの特徴である、変数を継続して実行するために、必要な変数は Envc に格納する。
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
6 コードに (next : Envc → t) と (exit : Envc → t) を引数に受け取っている。
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
7 これで次の遷移先を引数として受け取る事で、実行を継続していることを示す。
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
8 = の後は next Envc もしくは exit Envc となっていることからも
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
9 実行を継続している事が分かる。