@@ -232,10 +232,6 @@ instance Semigroup (List a) where
232232instance Monoid (List a) where
233233 neutral = []
234234
235−-- XXX: unification failure
236−-- instance VerifiedSemigroup (List a) where
237−-- semigroupOpIsAssociative = appendAssociative
238−
239235instance Functor List where
240236 map f [] = []
241237 map f (x::xs) = f x :: map f xs
@@ -811,6 +807,13 @@ hasAnyByNilFalse p (x::xs) =
811807hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
812808hasAnyNilFalse l = ?hasAnyNilFalseBody
813809
810+instance VerifiedSemigroup (List a) where
811+ semigroupOpIsAssociative = appendAssociative
812+
813+instance VerifiedMonoid (List a) where
814+ monoidNeutralIsNeutralL = appendNilRightNeutral
815+ monoidNeutralIsNeutralR xs = Refl
816+
814817--------------------------------------------------------------------------------
815818-- Proofs
816819--------------------------------------------------------------------------------