search

coq-community / coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
https://coq-community.org/coq-ext-lib/
BSD 2-Clause "Simplified" License
129 stars 46 forks source link

Right Idenity in MonadLaw #117

Closed mukeshtiwari closed 3 years ago

mukeshtiwari commented 3 years ago

In the MonadLaw, there is no right identity but based on my understanding, so far, we need to have left identity, right identity, and associativity. Is it a deliberate decision (or I am missing something)?

https://github.com/coq-community/coq-ext-lib/blob/aeb71ca2f5e5538f23f287772d3d84b35241415a/theories/Structures/MonadLaws.v#L22

[1] Haskell Monad Law Page

Lysxia commented 3 years ago

You're right, there should be that extra law.

liyishuai commented 3 years ago

Not sure why I removed it in 80d98c8d94dba49e934a1e2f4533f75097f22ed1. Worth adding back.

mukeshtiwari commented 3 years ago

@liyishuai I see you have released a new version, 0.11.4, on 23 September but you fixed this issue on 27 September. I have a code base that depends on coq-ext-lib for Monads so would it possible for you to release a new version, with this fix? Thanks in advance.

liyishuai commented 3 years ago

coq/opam-coq-archive#1884