@@ -108,6 +108,40 @@ length (x::xs) = 1 + length xs
108108(++) [] right = right
109109(++) (x::xs) right = x :: (xs ++ right)
110110
111+--------------------------------------------------------------------------------
112+-- Instances
113+--------------------------------------------------------------------------------
114+
115+instance (Eq a) => Eq (List a) where
116+ (==) [] [] = True
117+ (==) (x::xs) (y::ys) =
118+ if x == y then
119+ xs == ys
120+ else
121+ False
122+ (==) _ _ = False
123+
124+
125+instance Ord a => Ord (List a) where
126+ compare [] [] = EQ
127+ compare [] _ = LT
128+ compare _ [] = GT
129+ compare (x::xs) (y::ys) =
130+ if x /= y then
131+ compare x y
132+ else
133+ compare xs ys
134+
135+instance Semigroup (List a) where
136+ (<+>) = (++)
137+
138+instance Monoid (List a) where
139+ neutral = []
140+
141+-- XXX: unification failure
142+-- instance VerifiedSemigroup (List a) where
143+-- semigroupOpIsAssociative = appendAssociative
144+
111145--------------------------------------------------------------------------------
112146-- Zips and unzips
113147--------------------------------------------------------------------------------
@@ -171,8 +205,12 @@ foldr f e (x::xs) = f x (foldr f e xs)
171205-- Special folds
172206--------------------------------------------------------------------------------
173207
208+mconcat : Monoid a => List a -> a
209+mconcat = foldr (<+>) neutral
210+
174211concat : List (List a) -> List a
175−concat = foldr (++) []
212+concat [] = []
213+concat (x::xs) = x ++ concat xs
176214
177215concatMap : (a -> List b) -> List a -> List b
178216concatMap f [] = []
@@ -494,40 +532,6 @@ hasAnyByNilFalse p (x::xs) =
494532
495533hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
496534hasAnyNilFalse 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
531535
532536--------------------------------------------------------------------------------
533537-- Proofs
@@ -591,20 +595,21 @@ mapPreservesLengthStepCase = proof {
591595 trivial;
592596}
593597
594−prelude.list.zipWithTailProof = proof {
598+zipWithTailProof = proof {
595599 intros;
596600 rewrite (succInjective (length xs) (length ys) p);
597601 trivial;
598602}
599603
600−prelude.list.zipWith3TailProof = proof {
604+zipWith3TailProof = proof {
601605 intros;
602606 rewrite (succInjective (length xs) (length ys) p);
603607 trivial;
604608}
605609
606−prelude.list.zipWith3TailProof' = proof {
610+zipWith3TailProof' = proof {
607611 intros;
608612 rewrite (succInjective (length ys) (length zs) q);
609613 trivial;
610614}
615+