Idris2Doc : Data.List.Reverse

# 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