Idris2Doc : Data.List.TailRec

Data.List.TailRec

Contains:

1. Tail recursive versions of the list processing functions from
   Data.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.

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