Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/sources.tex @ 100:ebe838b83ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Self review
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 11:52:20 +0900
parents 54cf3b3153fe
children
comparison
equal deleted inserted replaced
99:a891d7551bbf 100:ebe838b83ada
7 7
8 \lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda.replaced} 8 \lstinputlisting[label=src:agda-subtype, caption=Agda 上で定義した CbC の部分型の定義(subtype.agda)] {src/subtype.agda.replaced}
9 9
10 \section{ノーマルレベル計算の実行} 10 \section{ノーマルレベル計算の実行}
11 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。 11 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
12 CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。 12 CbC のコードにより近づけるよう Agda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。
13 13
14 \lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced} 14 \lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced}
15 15
16 \section{メタレベル計算の実行} 16 \section{メタレベル計算の実行}
17 \ref{section:meta-level-exec}節で取り上げたソースコードをリスト~\ref{src:meta-level-exec}に示す。 17 \ref{section:meta-level-exec}節で取り上げたソースコードをリスト~\ref{src:meta-level-exec}に示す。