Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.agda @ 103:a271f3ff1922

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
102:9c62373bd474 103:a271f3ff1922
320 delta-fmap f (delta x (delta-bind ds tailDelta)) ≡⟨ refl ⟩ 320 delta-fmap f (delta x (delta-bind ds tailDelta)) ≡⟨ refl ⟩
321 delta-fmap f (delta (headDelta (delta x d)) (delta-bind ds tailDelta)) ≡⟨ refl ⟩ 321 delta-fmap f (delta (headDelta (delta x d)) (delta-bind ds tailDelta)) ≡⟨ refl ⟩
322 delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩ 322 delta-fmap f (delta-mu (delta (delta x d) ds)) ≡⟨ refl ⟩
323 (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎ 323 (delta-fmap f ∙ delta-mu) (delta (delta x d) ds) ∎
324 324
325 delta-is-monad : {l : Level} {A : Set l} -> Monad {l} {A} Delta delta-is-functor 325 delta-is-monad : {l : Level} -> Monad {l} Delta delta-is-functor
326 delta-is-monad = record { eta = delta-eta; 326 delta-is-monad = record { eta = delta-eta;
327 mu = delta-mu; 327 mu = delta-mu;
328 return = delta-eta; 328 return = delta-eta;
329 bind = delta-bind; 329 bind = delta-bind;
330 association-law = monad-law-1; 330 association-law = monad-law-1;