Mercurial > hg > Members > atton > delta_monad
diff agda/delta/monad.agda @ 115:e6bcc7467335
Temporary commit : Proving association-law ...
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Feb 2015 17:06:55 +0900 |
parents | d47aea3f9246 |
children | e1900c89dea9 |
line wrap: on
line diff
--- a/agda/delta/monad.agda Fri Jan 30 22:17:46 2015 +0900 +++ b/agda/delta/monad.agda Sun Feb 01 17:06:55 2015 +0900 @@ -147,6 +147,7 @@ return = delta-eta; bind = delta-bind; eta-is-nt = delta-eta-is-nt; + mu-is-nt = delta-mu-is-nt; association-law = monad-law-1; left-unity-law = delta-left-unity-law ; right-unity-law = \x -> (sym (delta-right-unity-law x)) }