changeset 6:3be2444dacc5

fix invisible header
author ryokka
date Thu, 26 Oct 2017 15:04:10 +0900
parents 8f91a416343d
children c0a6124f436b
files midterm/midterm.pdf midterm/midterm.tex
diffstat 2 files changed, 5 insertions(+), 22 deletions(-) [+]
line wrap: on
line diff
Binary file midterm/midterm.pdf has changed
--- a/midterm/midterm.tex	Thu Oct 26 14:35:55 2017 +0900
+++ b/midterm/midterm.tex	Thu Oct 26 15:04:10 2017 +0900
@@ -1,17 +1,12 @@
-%% TODO Agdaに関してやったこと書く
-%% TODO AgdaのStackとcbcのstackを例として出す。
-%% TODO 自然演繹の推論規則を表にまとめて乗っける
-
-
 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
 \usepackage[dvipdfmx]{graphicx}
 \usepackage{picins}
-\usepackage{listings,jlisting}
 \usepackage{fancyhdr}
+%\pagestyle{fancy}
 %\usepackage{abstract}
-%\pagestyle{fancy}
 \usepackage{url}
 \usepackage{bussproofs}
+\usepackage{listings,jlisting}
 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
 \rhead{}
 \cfoot{}
@@ -26,18 +21,9 @@
 \setlength{\footskip}{0mm}
 \pagestyle{empty}
 
-%% \lstset{%
-%%    breaklines=true
-%% }
-
 \lstset{
   frame=single,
   keepspaces=true,
-  stringstyle={\ttfamily},
-  commentstyle={\ttfamily},
-  identifierstyle={\ttfamily},
-  keywordstyle={\ttfamily},
-  basicstyle={\ttfamily},
   breaklines=true,
   xleftmargin=0zw,
   xrightmargin=0zw,
@@ -51,15 +37,13 @@
 
 
 \input{dummy.tex}
-\renewcommand{\abstractname}{Abstract}
+%\renewcommand{\abstractname}{Abstract}
 \begin{document}
-
 \title{CbC言語によるプログラムの検証}
-
 \author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
 \date{}
-
 \maketitle
+\thispagestyle{fancy}
 
 \section{研究目的}
 
@@ -310,12 +294,11 @@
 
 %% \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced}
 
-
 \section{今後の課題}
 現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。
 今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。
 
-\nocite{*}
+%\nocite{*}
 \bibliographystyle{junsrt}
 \bibliography{reference}
 \end{document}