Mercurial > hg > Members > atton > delta_monad
diff agda/delta.agda @ 90:55d11ce7e223
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 |
line wrap: on
line diff
--- a/agda/delta.agda Mon Jan 19 11:48:41 2015 +0900 +++ b/agda/delta.agda Mon Jan 19 12:11:38 2015 +0900 @@ -42,7 +42,7 @@ eta : {l : Level} {A : Set l} -> A -> Delta A eta x = mono x -bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B +bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B bind (mono x) f = f x bind (delta x d) f = delta (headDelta (f x)) (bind d (tailDelta ∙ f)) @@ -60,7 +60,7 @@ return : {l : Level} {A : Set l} -> A -> Delta A return = eta -_>>=_ : {l ll : Level} {A : Set l} {B : Set ll} -> +_>>=_ : {l : Level} {A B : Set l} -> (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) (mono x) >>= f = f x (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))