Mercurial > hg > Members > atton > delta_monad
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}