Mercurial > hg > Members > atton > delta_monad

diff agda/deltaM.agda @ 115:e6bcc7467335

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Temporary commit : Proving association-law ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 01 Feb 2015 17:06:55 +0900
parents 0a3b6cb91a05
children f02c5ad4a327
line wrap: on
line diff
--- a/agda/deltaM.agda	Fri Jan 30 22:17:46 2015 +0900
+++ b/agda/deltaM.agda	Sun Feb 01 17:06:55 2015 +0900
@@ -41,6 +41,10 @@
 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd)
 
 
+dmap : {l : Level} {A B : Set l} {n : Nat}
+       {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} ->
+       (M A -> B) -> DeltaM M {functorM} {monadM} A (S n) -> Delta B (S n)
+dmap f (deltaM d) = delta-fmap f d
 
 
 -- functor definitions