Mercurial > hg > Papers > 2017 > atton-master

changeset 49:7f1b5c33b282

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add agda.tex
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Mon, 30 Jan 2017 16:59:53 +0900
parents 623c90a21227
children 451c510825de
files paper/agda.tex paper/atton-master.tex
diffstat 2 files changed, 11 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- /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}
+
--- 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{ノーマルレベル計算の実行}