# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485763193 -32400
# Node ID 7f1b5c33b28203c0c33cabb5f9f3b69f13bb564d
# Parent  623c90a21227209e9c885c440161b32234546a88
Add agda.tex

diff -r 623c90a21227 -r 7f1b5c33b282 paper/agda.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/agda.tex	Mon Jan 30 16:59:53 2017 +0900
@@ -0,0 +1,7 @@
+\chapter{証明支援系言語 Agda による証明手法}
+\label{chapter:agda}
+\section{依存型を持つ証明支援系言語 Agda}
+\section{Natural Deduction}
+\section{Curry-Howard Isomorphism}
+\section{Reasoning}
+
diff -r 623c90a21227 -r 7f1b5c33b282 paper/atton-master.tex
--- a/paper/atton-master.tex	Mon Jan 30 16:41:56 2017 +0900
+++ b/paper/atton-master.tex	Mon Jan 30 16:59:53 2017 +0900
@@ -115,18 +115,13 @@
 %chapters
 \input{introduction.tex}
 
-\input{cbc.tex}
-\input{type.tex}
+%\input{cbc.tex}
+%\input{type.tex}
+\input{agda.tex}
 
-\chapter{証明支援系言語 Agda による証明手法}
-\label{chapter:agda}
-\section{依存型を持つ証明支援系言語 Agda}
-\section{Natural Deduction}
-\section{Curry-Howard Isomorphism}
-\section{Reasoning}
 
 \chapter{Agda における Continuation based C の表現}
-\label{chapter:subtype}
+\label{chapter:cbc-type}
 \section{CodeSegment の定義}
 \section{DataSegment の定義}
 \section{ノーマルレベル計算の実行}