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)) }