Mercurial > hg > Papers > 2015 > atton-thesis

changeset 55:43213dcf8d24

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add proof DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 16 Feb 2015 13:47:50 +0900
parents bf136bd59e7a
children 398b42a1ac19
files delta_with_monad.tex main.tex proof_deltaM.tex
diffstat 3 files changed, 11 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/delta_with_monad.tex	Mon Feb 16 12:40:53 2015 +0900
+++ b/delta_with_monad.tex	Mon Feb 16 13:47:50 2015 +0900
@@ -136,7 +136,7 @@
 
 このように、Monad と組み合せることでトレースを得ることができた。
 Writer 以外にも任意の Monad に対して DeltaM が Monad 則を満たす。
-この証明は非常に長いので付録に載せるものとする。% TODO ref
+この証明は非常に長いので付録\ref{section:proof_deltaM}に載せるものとする。
 
 DeltaM を定義した結果、Delta Monadと Monad を組み合せることができた。
 
--- a/main.tex	Mon Feb 16 12:40:53 2015 +0900
+++ b/main.tex	Mon Feb 16 13:47:50 2015 +0900
@@ -94,6 +94,6 @@
 % 付録
 \appendix
 \input{original_sources}
-% \input{proof_deltaM}
+\input{proof_deltaM}
 
 \end{document}
--- a/proof_deltaM.tex	Mon Feb 16 12:40:53 2015 +0900
+++ b/proof_deltaM.tex	Mon Feb 16 13:47:50 2015 +0900
@@ -1,4 +1,5 @@
-\section{DeltaM が Monad 則を満たす証明}
+\chapter{DeltaM が Monad 則を満たす証明}
+\label{section:proof_deltaM}
 DeltaM に対する Monad 則の証明も Agda によって行なう。
 プログラム内部のDeltaのバージョン数は全て同じであるとし、1以上とする。
 
@@ -11,10 +12,10 @@
 DeltaM に対する Monad 則の証明がリスト\ref{src:deltaM_is_monad}である。
 なお、Functor則に対する証明も行なったが省略する。
 
-\begin{table}
-    \lstinputlisting[basicstyle={\scriptsize},
-                     numberstyle={\tiny},
-                     label=src:deltaM_is_monad,
-                     caption= DeltaM が Monad 則を満たす証明]
-                     {src/deltaM_is_monad.agda.replaced}
-\end{table}
+
+\lstinputlisting[basicstyle={\scriptsize},
+                 numberstyle={\tiny},
+                 label=src:deltaM_is_monad,
+                 caption= DeltaM が Monad 則を満たす証明]
+                 {src/deltaM_is_monad.agda.replaced}
+