Mercurial > hg > Members > atton > delta_monad

changeset 122:e1900c89dea9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix Monad-proof for Delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 12:12:14 +0900
parents 673e1ca0d1a9
children ee7f5162ec1f
files agda/delta/monad.agda
diffstat 1 files changed, 0 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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;