Mercurial > hg > Members > atton > delta_monad

comparison 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
comparison
equal deleted inserted replaced
114:08403eb8db8b 115:e6bcc7467335
39 DeltaM M {functorM} {monadM} A (S m) -> 39 DeltaM M {functorM} {monadM} A (S m) ->
40 DeltaM M {functorM} {monadM} A ((S n) + (S m)) 40 DeltaM M {functorM} {monadM} A ((S n) + (S m))
41 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) 41 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd)
42 42
43 43
44 dmap : {l : Level} {A B : Set l} {n : Nat}
45 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} ->
46 (M A -> B) -> DeltaM M {functorM} {monadM} A (S n) -> Delta B (S n)
47 dmap f (deltaM d) = delta-fmap f d
44 48
45 49
46 -- functor definitions 50 -- functor definitions
47 open Functor 51 open Functor
48 deltaM-fmap : {l : Level} {A B : Set l} {n : Nat} 52 deltaM-fmap : {l : Level} {A B : Set l} {n : Nat}