idris-lang/Idris-dev — pull request #1694 by reynir (2014-11-03 15:58:42+00:00)
Title: VerifiedSemigroup, VerifiedMonoid for List

After implementing `VerifiedSemigroup (List a)` myself (reynir/Verified@7c42d6e6105335c72c732d13b9004cb4474c9f0a) I noticed there was an outcommented implementation in Prelude.List saying "unification failure".

Anyway, it works now, and I also added a VerifiedMonoid instance. Both are very simple.

There's some disagreement about what is left and right neutral in the names which looks odd in the VerifiedMonoid instance, namely `monoidNeutralIsNeutralL = appendNilRightNeutral`