diff --git a/src/Solutions/DataTypes.idr b/src/Solutions/DataTypes.idr index cdcb982b..ac1cfd95 100644 --- a/src/Solutions/DataTypes.idr +++ b/src/Solutions/DataTypes.idr @@ -190,6 +190,10 @@ filterList f Nil = Nil filterList f (x :: xs) = if f x then x :: filterList f xs else filterList f xs +(++) : List a -> List a -> List a +(++) Nil ys = ys +(++) (x :: xs) ys = x :: (Solutions.DataTypes.(++) xs ys) + headMaybe : List a -> Maybe a headMaybe Nil = Nothing headMaybe (x :: _) = Just x diff --git a/src/Tutorial/DataTypes.md b/src/Tutorial/DataTypes.md index 7dd08e84..7280e916 100644 --- a/src/Tutorial/DataTypes.md +++ b/src/Tutorial/DataTypes.md @@ -1212,6 +1212,14 @@ signature are treated as type parameters. total filterList : (a -> Bool) -> List a -> List a + -- re-implement list concatenation (++) such that e.g. (++) [1, 2] [3, 4] = [1, 2, 3, 4] + -- note that because this function conflicts with the standard + -- Prelude.List.(++), if you use it then you will need to prefix it with + -- the name of your module, like DataTypes.(++) or Ch3.(++). alternatively + -- you could simply call the function something unique like myListConcat or concat' + total + (++) : List a -> List a -> List a + -- return the first value of a list, if it is non-empty total headMaybe : List a -> Maybe a