Mercurial > hg > Members > atton > delta_monad
diff agda/delta/monad.agda @ 103:a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Jan 2015 14:08:46 +0900 |
| parents | dfe8c67390bd |
| children | ebd0d6e2772c |
line wrap: on
line diff
--- a/agda/delta/monad.agda Sun Jan 25 12:16:34 2015 +0900 +++ b/agda/delta/monad.agda Mon Jan 26 14:08:46 2015 +0900 @@ -322,7 +322,7 @@ delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩ (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎ -delta-is-monad : {l : Level} {A : Set l} -> Monad {l} {A} Delta delta-is-functor +delta-is-monad : {l : Level} -> Monad {l} Delta delta-is-functor delta-is-monad = record { eta = delta-eta; mu = delta-mu; return = delta-eta;