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:6959} : 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:7366} : 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