# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423966113 -32400
# Node ID 2bf1fa6d2006d06c34928363ca5a63b6ea28d52d
# Parent  b6dcbe8617a93fc9e8537adc76fc8098d4631f4d
Adjust codes

diff -r b6dcbe8617a9 -r 2bf1fa6d2006 agda/delta.agda
--- a/agda/delta.agda	Sun Feb 15 10:15:10 2015 +0900
+++ b/agda/delta.agda	Sun Feb 15 11:08:33 2015 +0900
@@ -54,4 +54,4 @@
         (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n)
 d >>= f = delta-bind d f
 
--}
\ No newline at end of file
+-}
diff -r b6dcbe8617a9 -r 2bf1fa6d2006 agda/delta/monad.agda
--- a/agda/delta/monad.agda	Sun Feb 15 10:15:10 2015 +0900
+++ b/agda/delta/monad.agda	Sun Feb 15 11:08:33 2015 +0900
@@ -69,10 +69,10 @@
     (delta-fmap delta-mu
      (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))
   ∎
-delta-fmap-mu-to-tail (S n) (S n₁) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin
+delta-fmap-mu-to-tail (S n) (S m) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin
   delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
     (delta-fmap tailDelta (delta-fmap delta-mu dds))
-  ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S n₁) dds) ⟩
+  ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S m) dds) ⟩
   delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
     (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds)))
   ∎
@@ -83,7 +83,7 @@
 -- association-law : join . delta-fmap join = join . join
 delta-association-law : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
               ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
-delta-association-law {n =       O} (mono d)                          = refl
+delta-association-law {n =   O} (mono d)                          = refl
 delta-association-law {n = S n} (delta (delta (delta x d) dd) ds) = begin
   delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
   ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩