Mercurial > hg > Papers > 2015 > atton-thesis

changeset 39:8a70394e45b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add record of functor in agda
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 12 Feb 2015 18:08:01 +0900
parents a5bb7a7cc0e1
children 470d99799398
files fig/delta_example.xbb fig/functor.xbb fig/functor_in_haskell.xbb fig/monad_laws.xbb fig/morphism_composition_law.xbb fig/natural_transformation.xbb fig/natural_transformation_in_haskell.xbb fig/non_delta_example.xbb fig/ryukyu.xbb fig/simple_category.xbb main.tex replace_agda.rb
diffstat 12 files changed, 12 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/fig/delta_example.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/delta_example.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 559.000000 279.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/functor.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/functor.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 545.000000 456.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/functor_in_haskell.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/functor_in_haskell.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 324.000000 176.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/monad_laws.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/monad_laws.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 464.000000 137.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/morphism_composition_law.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/morphism_composition_law.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 412.000000 273.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/natural_transformation.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/natural_transformation.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 211.000000 136.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/natural_transformation_in_haskell.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/natural_transformation_in_haskell.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 322.000000 136.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/non_delta_example.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/non_delta_example.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 504.000000 244.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/ryukyu.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/ryukyu.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 595.000000 842.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/fig/simple_category.xbb	Thu Feb 12 17:49:35 2015 +0900
+++ b/fig/simple_category.xbb	Thu Feb 12 18:08:01 2015 +0900
@@ -4,5 +4,5 @@
 %%HiResBoundingBox: 0.000000 0.000000 205.000000 82.000000
 %%PDFVersion: 1.3
 %%Pages: 1
-%%CreationDate: Mon Feb  9 09:44:36 2015
+%%CreationDate: Thu Feb 12 18:06:21 2015
 
--- a/main.tex	Thu Feb 12 17:49:35 2015 +0900
+++ b/main.tex	Thu Feb 12 18:08:01 2015 +0900
@@ -77,12 +77,7 @@
 \input{category}
 \input{functional_programming}
 \input{agda}
-
-\chapter{Delta が Monad である証明}
-\section{Agda における Functor 則}
-\section{Agda における Monad 則}
-\section{Delta が Functor 則を満たす証明}
-\section{Delta が Monad 則を満たす証明}
+\input{proof_delta}
 
 \chapter{任意の Monad と Delta の組み合せ}
 \section{Monad と組み合せた Delta である DeltaM の定義}
--- a/replace_agda.rb	Thu Feb 12 17:49:35 2015 +0900
+++ b/replace_agda.rb	Thu Feb 12 18:08:01 2015 +0900
@@ -1,8 +1,7 @@
 #!/usr/bin/env ruby
 
-require 'pry'
-
 replace_table = {
+  '∙' => 'circ',
   '⟨' => 'langle',
   '⟩' => 'rangle',
   '∎' => 'blacksquare'