Idris2Doc : Data.List.Equalities

Data.List.Equalities

SnocNonEmpty : (xs : Lista) -> (x : a) -> NonEmpty (snocxsx)
Proof that snoc'ed list is not empty in terms of `NonEmpty`.
Totality: total
appendCong2 : x1 = y1 -> x2 = y2 -> x1++x2 = y1++y2
Appending pairwise equal lists gives equal lists
Totality: total
appendNonEmptyLeftNotEq : (zs : Lista) -> (xs : Lista) -> NonEmptyxs => Not (zs = xs++zs)
List cannot be equal to itself prepended with some non-empty list.
Totality: total
appendNonEmptyRightNotEq : (zs : Lista) -> (xs : Lista) -> NonEmptyxs => Not (zs = zs++xs)
List cannot be equal to itself appended with some non-empty list.
Totality: total
appendSameLeftInjective : (xs : Lista) -> (ys : Lista) -> (zs : Lista) -> zs++xs = zs++ys -> xs = ys
Appending the same list at left is injective.
Totality: total
appendSameRightInjective : (xs : Lista) -> (ys : Lista) -> (zs : Lista) -> xs++zs = ys++zs -> xs = ys
Appending the same list at right is injective.
Totality: total
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
lengthDistributesOverAppend : (xs : Lista) -> (ys : Lista) -> length (xs++ys) = lengthxs+lengthys
List.length is distributive over appending.
Totality: total
lengthSnoc : (x : a) -> (xs : Lista) -> length (snocxsx) = S (lengthxs)
Length of a snoc'd list is the same as Succ of length list.
Totality: total
mapDistributesOverAppend : (f : (a -> b)) -> (xs : Lista) -> (ys : Lista) -> mapf (xs++ys) = mapfxs++mapfys
List.map is distributive over appending.
Totality: total
snocInjective : snocxsx = snocysy -> (xs = ys, x = y)
Equal non-empty lists should result in equal components after destructuring 'snoc'.
Totality: total
snocNonEmpty : xs++ [x] = Nil -> Void
A list constructued using snoc cannot be empty.
Totality: total