@@ -232,10 +232,6 @@ instance Semigroup (List a) where
232instance Monoid (List a) where
232instance Monoid (List a) where
233 neutral = []
233 neutral = []
235−-- XXX: unification failure
236−-- instance VerifiedSemigroup (List a) where
237−-- semigroupOpIsAssociative = appendAssociative
239instance Functor List where
235instance Functor List where
240 map f [] = []
236 map f [] = []
241 map f (x::xs) = f x :: map f xs
237 map f (x::xs) = f x :: map f xs
@@ -811,6 +807,13 @@ hasAnyByNilFalse p (x::xs) =
811hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
807hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
812hasAnyNilFalse l = ?hasAnyNilFalseBody
808hasAnyNilFalse l = ?hasAnyNilFalseBody
810+instance VerifiedSemigroup (List a) where
811+ semigroupOpIsAssociative = appendAssociative
813+instance VerifiedMonoid (List a) where
814+ monoidNeutralIsNeutralL = appendNilRightNeutral
815+ monoidNeutralIsNeutralR xs = Refl
814--------------------------------------------------------------------------------
817--------------------------------------------------------------------------------
816--------------------------------------------------------------------------------
819--------------------------------------------------------------------------------