Data.List.Reverse

Properties of the reverse function.

Definitions

reverseOntoAcc : (xs : List a) -> (ys : List a) -> (zs : List a) -> reverseOnto (ys ++ zs) xs = reverseOnto ys xs ++ zs

Totality: total
Visibility: export

reverseOntoSpec : (xs : List a) -> (ys : List a) -> reverseOnto xs ys = reverse ys ++ xs

  Serves as a specification for reverseOnto.

Totality: total
Visibility: export

reverseNil : reverse [] = []

  The reverse of an empty list is an empty list.  Together with reverseCons,
  serves as a specification for reverse.

Totality: total
Visibility: export

reverseCons : (x : a) -> (xs : List a) -> reverse (x :: xs) = snoc (reverse xs) x

  The reverse of a cons is the reverse of the tail followed by the head.
  Together with reverseNil serves as a specification for reverse.

Totality: total
Visibility: export

0 slowReverse : List a -> List a

  A slow recursive definition of reverse.

Totality: total
Visibility: public export

reverseEquiv : (xs : List a) -> slowReverse xs = reverse xs

  The iterative and recursive defintions of reverse are the same.

Totality: total
Visibility: export

reverseSingletonId : (x : a) -> reverse [x] = [x]

  Reversing a singleton list is a no-op.

Totality: total
Visibility: export

reverseOntoLength : (xs : List a) -> (acc : List a) -> length (reverseOnto acc xs) = length acc + length xs

  Reversing onto preserves list length.

Totality: total
Visibility: export

reverseLength : (xs : List a) -> length (reverse xs) = length xs

  Reversing preserves list length.

Totality: total
Visibility: export

reverseEqual : (xs : List a) -> (ys : List a) -> reverse xs = reverse ys -> xs = ys

  Equal reversed lists are equal.

Totality: total
Visibility: export