Idris2Doc : Data.List.Reverse

Data.List.Reverse

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 : reverseNil = Nil
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