idris-lang/Idris-dev — pull request #1384 by lenary (2014-07-15 19:57:46+00:00)
Title: Verified Bounded Semilattices are incorrect

I believe the propositions here: https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Algebra.idr#L179-L219 are slightly incorrect.

I think they should be, respectively: `join e bottom = e` and `meet e top = e`, given that top and bottom are supposed to be unital for meet and join respectively.

I can do a (very simple) PR if need be.