Mercurial > hg > Members > atton > delta_monad
changeset 137:2bf1fa6d2006
Adjust codes
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 15 Feb 2015 11:08:33 +0900 |
| parents | b6dcbe8617a9 |
| children | 1f218e2d9de0 |
| files | agda/delta.agda agda/delta/monad.agda |
| diffstat | 2 files changed, 4 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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 +-}
--- 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) ⟩