Idris2Doc : Data.List.Reverse

# Data.List.Reverse

`Properties of the reverse function.`
reverseCons : (x : a) -> (xs : Lista) -> reverse (x::xs) = snoc (reversexs) 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
reverseEqual : (xs : Lista) -> (ys : Lista) -> reversexs = reverseys -> xs = ys
`  Equal reversed lists are equal.`

Totality: total
reverseEquiv : (xs : Lista) -> slowReversexs = reversexs
`  The iterative and recursive defintions of reverse are the same.`

Totality: total
reverseLength : (xs : Lista) -> length (reversexs) = lengthxs
`  Reversing preserves list length.`

Totality: total
reverseNil : reverse [] = []
`  The reverse of an empty list is an empty list. Together with reverseCons,  serves as a specification for reverse.`

Totality: total
reverseOntoAcc : (xs : Lista) -> (ys : Lista) -> (zs : Lista) -> reverseOnto (ys++zs) xs = reverseOntoysxs++zs
Totality: total
reverseOntoLength : (xs : Lista) -> (acc : Lista) -> length (reverseOntoaccxs) = lengthacc+lengthxs
`  Reversing onto preserves list length.`

Totality: total
reverseOntoSpec : (xs : Lista) -> (ys : Lista) -> reverseOntoxsys = reverseys++xs
`  Serves as a specification for reverseOnto.`

Totality: total
reverseSingletonId : (x : a) -> reverse [x] = [x]
`  Reversing a singleton list is a no-op.`

Totality: total
slowReverse : Lista -> Lista
`  A slow recursive definition of reverse.`

Totality: total