Idris2Doc : Data.List.TailRec

# Data.List.TailRec

```Contains:

1. Tail recursive versions of the list processing functions from
List.

2. Extensional equality proofs that these variants are
(extensionally) equivalent to their non-tail-recursive
counterparts.

Note:

1. Written in one sitting, feel free to refactor

2. The proofs below also work on non-publicly exported
definitions.  This could be due to a bug, and will need to be
moved elsewhere if it's fixed.
```

## Definitions

`length : List a -> Nat`
Totality: total
Visibility: export
`length_ext : (xs : List a) -> length xs = length xs`
Totality: total
Visibility: export
`take : Nat -> List a -> List a`
Totality: total
Visibility: export
`take_ext : (n : Nat) -> (xs : List a) -> take n xs = take n xs`
Totality: total
Visibility: export
`span : (a -> Bool) -> List a -> (List a, List a)`
Totality: total
Visibility: export
`span_ext : (p : (a -> Bool)) -> (xs : List a) -> span p xs = span p xs`
Totality: total
Visibility: export
`break : (a -> Bool) -> List a -> (List a, List a)`
Totality: total
Visibility: export
`break_ext : (p : (a -> Bool)) -> (xs : List a) -> break p xs = break p xs`
Totality: total
Visibility: export
`split : (a -> Bool) -> List a -> List1 (List a)`
Totality: total
Visibility: export
`split_ext : (p : (a -> Bool)) -> (xs : List a) -> split p xs = split p xs`
Totality: total
Visibility: export
`splitAt : Nat -> List a -> (List a, List a)`
Totality: total
Visibility: export
`splitAt_ext : (n : Nat) -> (xs : List a) -> splitAt n xs = splitAt n xs`
Totality: total
Visibility: export
`partition : (a -> Bool) -> List a -> (List a, List a)`
Totality: total
Visibility: export
`intersperse : a -> List a -> List a`
Totality: total
Visibility: export
`intersperse_ext : (sep : a) -> (xs : List a) -> intersperse sep xs = intersperse sep xs`
Totality: total
Visibility: export
`mapMaybe : (a -> Maybe b) -> List a -> List b`
Totality: total
Visibility: export
`mapMaybe_ext : (f : (a -> Maybe b)) -> (xs : List a) -> mapMaybe f xs = mapMaybe f xs`
Totality: total
Visibility: export
`sorted : Ord a => List a -> Bool`
Totality: total
Visibility: export
`sorted_ext : {auto {conArg:6976} : Ord a} -> (xs : List a) -> sorted xs = sorted xs`
Visibility: export
`mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a`
Totality: total
Visibility: export
`mergeBy_ext : (order : (a -> a -> Ordering)) -> (left : List a) -> (right : List a) -> mergeBy order left right = mergeBy order left right`
Visibility: export
`merge : Ord a => List a -> List a -> List a`
Totality: total
Visibility: export
`merge_ext : {auto {conArg:7383} : Ord a} -> (left : List a) -> (right : List a) -> merge left right = merge left right`
Visibility: export
`sortBy : (a -> a -> Ordering) -> List a -> List a`
Totality: total
Visibility: export