# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1422846734 -32400
# Node ID e1900c89dea99f3a83c87264fe4ef2d02cd9b88d
# Parent  673e1ca0d1a953e6e67094dca4f4de72b7dc3d4b
Fix Monad-proof for Delta

diff -r 673e1ca0d1a9 -r e1900c89dea9 agda/delta/monad.agda
--- a/agda/delta/monad.agda	Mon Feb 02 12:11:24 2015 +0900
+++ b/agda/delta/monad.agda	Mon Feb 02 12:12:14 2015 +0900
@@ -144,8 +144,6 @@
 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n))  delta-is-functor
 delta-is-monad = record { eta    = delta-eta;
                           mu     = delta-mu;
-                          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;