@@ -378,7 +378,7 @@ scanl : (b -> a -> b) -> b -> List a -> List b
378scanl f q [] = [q]
378scanl f q [] = [q]
379scanl f q (x::xs) = q :: scanl f (f q x) xs
379scanl f q (x::xs) = q :: scanl f (f q x) xs
381−||| The scanl1 function is a variant of scanl that doesn't require an explicit
381+||| The scanl1 function is a variant of scanl that doesn't require an explicit
382||| starting value.
382||| starting value.
383||| It assumes the first element of the list to be the starting value and then
383||| It assumes the first element of the list to be the starting value and then
384||| starts the fold with the element following it.
384||| starts the fold with the element following it.
@@ -855,6 +855,10 @@ catMaybes (x::xs) =
855-- Properties
855-- Properties
856--------------------------------------------------------------------------------
856--------------------------------------------------------------------------------
858+||| (::) is injective
859+consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)
860+consInjective Refl = (Refl, Refl)
858||| The empty list is a right identity for append.
862||| The empty list is a right identity for append.
859appendNilRightNeutral : (l : List a) ->
863appendNilRightNeutral : (l : List a) ->
860 l ++ [] = l
864 l ++ [] = l