Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM.agda @ 90:55d11ce7e223

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unify levels on data type. only use suc to proofs
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 19 Jan 2015 12:11:38 +0900
parents 5411ce26d525
children bcd4fe52a504
comparison
equal deleted inserted replaced
89:5411ce26d525 90:55d11ce7e223
52 checkOut O (deltaM (mono x)) = x 52 checkOut O (deltaM (mono x)) = x
53 checkOut O (deltaM (delta x _)) = x 53 checkOut O (deltaM (delta x _)) = x
54 checkOut (S n) (deltaM (mono x)) = x 54 checkOut (S n) (deltaM (mono x)) = x
55 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d) 55 checkOut {l} {A} {M} {functorM} {monadM} (S n) (deltaM (delta _ d)) = checkOut {l} {A} {M} {functorM} {monadM} n (deltaM d)
56 56
57 {- 57
58 deltaM-fmap : {l ll : Level} {A : Set l} {B : Set ll} 58 open Functor
59 {M : {l' : Level} -> Set l' -> Set l'} 59 deltaM-fmap : {l : Level} {A B : Set l}
60 {functorM : {l' : Level} -> Functor {l'} M} 60 {M : {l' : Level} -> Set l' -> Set l'}
61 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} 61 {functorM : {l' : Level} -> Functor {l'} M}
62 -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B 62 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
63 deltaM-fmap {l} {ll} {A} {B} {M} {functorM} f (deltaM d) = deltaM (Functor.fmap delta-is-functor (Functor.fmap functorM f) d) 63 -> (A -> B) -> DeltaM M {functorM} {monadM} A -> DeltaM M {functorM} {monadM} B
64 -} 64 deltaM-fmap {l} {A} {B} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d)