Idris2Doc : Data.List.Equalities

# Data.List.Equalities

## Definitions

`snocNonEmpty : Not (xs ++ [x] = [])`
`  A list constructued using snoc cannot be empty.`

Totality: total
Visibility: export
`SnocNonEmpty : (xs : List a) -> (x : a) -> NonEmpty (snoc xs x)`
`  Proof that snoc'ed list is not empty in terms of `NonEmpty`.`

Totality: total
Visibility: export
`consCong2 : x = y -> xs = ys -> x :: xs = y :: ys`
`  Two lists are equal, if their heads are equal and their tails are equal.`

Totality: total
Visibility: export
`snocInjective : snoc xs x = snoc ys y -> (xs = ys, x = y)`
`  Equal non-empty lists should result in equal components after destructuring 'snoc'.`

Totality: total
Visibility: export
`appendCong2 : x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2`
`  Appending pairwise equal lists gives equal lists`

Totality: total
Visibility: export
`mapDistributesOverAppend : (f : (a -> b)) -> (xs : List a) -> (ys : List a) -> map f (xs ++ ys) = map f xs ++ map f ys`
`  List.map is distributive over appending.`

Totality: total
Visibility: export
`lengthDistributesOverAppend : (xs : List a) -> (ys : List a) -> length (xs ++ ys) = length xs + length ys`
`  List.length is distributive over appending.`

Totality: total
Visibility: export
`lengthSnoc : (x : a) -> (xs : List a) -> length (snoc xs x) = S (length xs)`
`  Length of a snoc'd list is the same as Succ of length list.`

Totality: total
Visibility: export
`appendSameLeftInjective : (xs : List a) -> (ys : List a) -> (zs : List a) -> zs ++ xs = zs ++ ys -> xs = ys`
`  Appending the same list at left is injective.`

Totality: total
Visibility: export
`appendSameRightInjective : (xs : List a) -> (ys : List a) -> (zs : List a) -> xs ++ zs = ys ++ zs -> xs = ys`
`  Appending the same list at right is injective.`

Totality: total
Visibility: export
`appendNonEmptyLeftNotEq : (zs : List a) -> (xs : List a) -> NonEmpty xs => Not (zs = xs ++ zs)`
`  List cannot be equal to itself prepended with some non-empty list.`

Totality: total
Visibility: export
`appendNonEmptyRightNotEq : (zs : List a) -> (xs : List a) -> NonEmpty xs => Not (zs = zs ++ xs)`
`  List cannot be equal to itself appended with some non-empty list.`

Totality: total
Visibility: export
`bindConcatPrf : (xs : List a) -> (x : a) -> (f : (a -> List b)) -> (x :: xs) >>= f = f x ++ (xs >>= f)`
`  Proof of correspondence between list bind and concatenation.`

Totality: total
Visibility: export