diff agda/deltaM.agda @ 116:f02c5ad4a327

Prove association-law for DeltaM by (S O) pattern with definition changes
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 01 Feb 2015 17:55:39 +0900
parents e6bcc7467335
children 53cb21845dea
line wrap: on
line diff
--- a/agda/deltaM.agda	Sun Feb 01 17:06:55 2015 +0900
+++ b/agda/deltaM.agda	Sun Feb 01 17:55:39 2015 +0900
@@ -69,9 +69,9 @@
                         {M : Set l -> Set l} {functorM : Functor  M} {monadM   : Monad  M functorM} ->
                         DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n)  ->
                         DeltaM M {functorM} {monadM} A (S n)
-deltaM-mu {n = O}   {functorM = fm} {monadM = mm} (deltaM (mono x))    = deltaM (mono (mu mm (fmap fm headDeltaM x)))
-deltaM-mu {n = S n} {functorM = fm} {monadM = mm} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
-                                                                                      (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))
+deltaM-mu {n = O}   {functorM = fm} {monadM = mm} d = deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))
+deltaM-mu {n = S n} {functorM = fm} {monadM = mm} d = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))
+                                                                   (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d)))
                                                   
 
 deltaM-bind : {l : Level} {A B : Set l}