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