@@ -2,6 +2,7 @@ module prelude.list
22
33import builtins
44
5+import prelude.algebra
56import prelude.maybe
67import prelude.nat
78
@@ -434,28 +435,6 @@ catMaybes (x::xs) =
434435 Nothing => catMaybes xs
435436 Just j => j :: catMaybes xs
436437
437−--------------------------------------------------------------------------------
438−-- Instances
439−--------------------------------------------------------------------------------
440−
441−instance (Eq a) => Eq (List a) where
442− (==) [] [] = True
443− (==) (a::restA) (b::restB) =
444− if a == b
445− then restA == restB
446− else False
447− (==) _ _ = False
448−
449−
450−instance Ord a => Ord (List a) where
451− compare [] [] = EQ
452− compare [] _ = LT
453− compare _ [] = GT
454− compare (a::restA) (b::restB) =
455− if a /= b
456− then compare a b
457− else compare restA restB
458−
459438--------------------------------------------------------------------------------
460439-- Properties
461440--------------------------------------------------------------------------------
@@ -469,7 +448,7 @@ appendNilRightNeutral (x::xs) =
469448 ?appendNilRightNeutralStepCase
470449
471450appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
472− (l ++ c) ++ r = l ++ (c ++ r)
451+ l ++ (c ++ r) = (l ++ c) ++ r
473452appendAssociative [] c r = refl
474453appendAssociative (x::xs) c r =
475454 let inductiveHypothesis = appendAssociative xs c r in
@@ -515,6 +494,40 @@ hasAnyByNilFalse p (x::xs) =
515494
516495hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
517496hasAnyNilFalse l = ?hasAnyNilFalseBody
497+
498+--------------------------------------------------------------------------------
499+-- Instances
500+--------------------------------------------------------------------------------
501+
502+instance (Eq a) => Eq (List a) where
503+ (==) [] [] = True
504+ (==) (x::xs) (y::ys) =
505+ if x == y then
506+ xs == ys
507+ else
508+ False
509+ (==) _ _ = False
510+
511+
512+instance Ord a => Ord (List a) where
513+ compare [] [] = EQ
514+ compare [] _ = LT
515+ compare _ [] = GT
516+ compare (x::xs) (y::ys) =
517+ if x /= y then
518+ compare x y
519+ else
520+ compare xs ys
521+
522+instance Semigroup (List a) where
523+ (<+>) = (++)
524+
525+instance Monoid (List a) where
526+ neutral = []
527+
528+-- XXX: unification failure
529+-- instance VerifiedSemigroup (List a) where
530+-- semigroupOpIsAssociative = appendAssociative
518531
519532--------------------------------------------------------------------------------
520533-- Proofs
@@ -595,4 +608,3 @@ prelude.list.zipWith3TailProof' = proof {
595608 rewrite (succInjective (length ys) (length zs) q);
596609 trivial;
597610}
598−