Mercurial > hg > Members > atton > delta_monad
comparison 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 |
comparison
equal
deleted
inserted
replaced
114:08403eb8db8b | 115:e6bcc7467335 |
---|---|
145 delta-is-monad = record { eta = delta-eta; | 145 delta-is-monad = record { eta = delta-eta; |
146 mu = delta-mu; | 146 mu = delta-mu; |
147 return = delta-eta; | 147 return = delta-eta; |
148 bind = delta-bind; | 148 bind = delta-bind; |
149 eta-is-nt = delta-eta-is-nt; | 149 eta-is-nt = delta-eta-is-nt; |
150 mu-is-nt = delta-mu-is-nt; | |
150 association-law = monad-law-1; | 151 association-law = monad-law-1; |
151 left-unity-law = delta-left-unity-law ; | 152 left-unity-law = delta-left-unity-law ; |
152 right-unity-law = \x -> (sym (delta-right-unity-law x)) } | 153 right-unity-law = \x -> (sym (delta-right-unity-law x)) } |
153 | 154 |
154 | 155 |