git.iko.soy/Idris-dev
on master help sign in
VerifiedSemigroup, VerifiedMonoid for List

* No unification failure for VerifiedSemigroup anymore * Add VerifiedMonoid (List a) instance Note that the instances need definitions from further down in the file and are thus moved closer to the end of the file.

commit715940e3cec075b5cc5a4b275d260034123914a8 authorReynir Björnsson <reynir@reynir.dk> dateMon 3 Nov 2014, 12:00 (12 years ago) parente63be93
1 file changed+7−4
compare with master
unifiedsplit
libs/prelude/Prelude/List.idr+7−4
libs/prelude/Prelude/List.idr+7−4
@@ -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--------------------------------------------------------------------------------