Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 116:f02c5ad4a327

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
115:e6bcc7467335 116:f02c5ad4a327
67 67
68 deltaM-mu : {l : Level} {A : Set l} {n : Nat} 68 deltaM-mu : {l : Level} {A : Set l} {n : Nat}
69 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> 69 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} ->
70 DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) -> 70 DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) ->
71 DeltaM M {functorM} {monadM} A (S n) 71 DeltaM M {functorM} {monadM} A (S n)
72 deltaM-mu {n = O} {functorM = fm} {monadM = mm} (deltaM (mono x)) = deltaM (mono (mu mm (fmap fm headDeltaM x))) 72 deltaM-mu {n = O} {functorM = fm} {monadM = mm} d = deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d))))
73 deltaM-mu {n = S n} {functorM = fm} {monadM = mm} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) 73 deltaM-mu {n = S n} {functorM = fm} {monadM = mm} d = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))
74 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))) 74 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d)))
75 75
76 76
77 deltaM-bind : {l : Level} {A B : Set l} 77 deltaM-bind : {l : Level} {A B : Set l}
78 {n : Nat} 78 {n : Nat}
79 {M : Set l -> Set l} 79 {M : Set l -> Set l}