Idris2Doc : Data.List

# Data.List

InBounds : Nat -> Lista -> Type
Satisfiable if `k` is a valid index into `xs`

@ k the potential index
@ xs the list into which k may be an index
Totality: total
Constructors:
InFirst : InBoundsZ (x::xs)
Z is a valid index into any cons cell
InLater : InBoundskxs -> InBounds (Sk) (x::xs)
Valid indices can be extended
NonEmpty : Lista -> Type
Totality: total
Constructor:
IsNonEmpty : NonEmpty (x::xs)
appendAssociative : (l : Lista) -> (c : Lista) -> (r : Lista) -> l++ (c++r) = (l++c) ++r
Appending lists is associative.
Totality: total
appendNilRightNeutral : (l : Lista) -> l++Nil = l
The empty list is a right identity for append.
Totality: total
break : (a -> Bool) -> Lista -> (Lista, Lista)
Totality: total
catMaybes : List (Maybea) -> Lista
Extract all of the values contained in a List of Maybes
Totality: total
consInjective : the (Lista) (x::xs) = the (Listb) (y::ys) -> (x = y, xs = ys)
(::) is injective
Totality: total
delete : Eqa => a -> Lista -> Lista
`delete x` removes the first occurrence of `x` from its list argument. For
example,

````idris example
delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
````

It is a special case of deleteBy, which allows the programmer to supply
their own equality test.
Totality: total
deleteBy : (a -> a -> Bool) -> a -> Lista -> Lista
The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
Totality: total
drop : Nat -> Lista -> Lista
Totality: total
dropFusion : (n : Nat) -> (m : Nat) -> (l : Listt) -> dropn (dropml) = drop (n+m) l
Totality: total
dropWhile : (a -> Bool) -> Lista -> Lista
Totality: total
elemBy : (a -> a -> Bool) -> a -> Lista -> Bool
Check if something is a member of a list using a custom comparison.
Totality: total
filter : (a -> Bool) -> Lista -> Lista
Totality: total
find : (a -> Bool) -> Lista -> Maybea
Find the first element of the list that satisfies the predicate.
Totality: total
foldl1 : (a -> a -> a) -> (l : Lista) -> {auto 0 _ : NonEmptyl} -> a
Foldl a non-empty list without seeding the accumulator.
@ ok proof that the list is non-empty
Totality: total
foldl1By : (b -> a -> b) -> (a -> b) -> (l : Lista) -> {auto 0 _ : NonEmptyl} -> b
Totality: total
foldr1 : (a -> a -> a) -> (l : Lista) -> {auto 0 _ : NonEmptyl} -> a
Foldr a non-empty list without seeding the accumulator.
@ ok proof that the list is non-empty
Totality: total
foldr1By : (a -> b -> b) -> (a -> b) -> (l : Lista) -> {auto 0 _ : NonEmptyl} -> b
Totality: total
head : (l : Lista) -> {auto 0 _ : NonEmptyl} -> a
Get the head of a non-empty list.
@ ok proof the list is non-empty
Totality: total
Attempt to get the head of a list. If the list is empty, return `Nothing`.
Totality: total
inBounds : (k : Nat) -> (xs : Lista) -> Dec (InBoundskxs)
Decide whether `k` is a valid index into `xs`
Totality: total
index : (n : Nat) -> (xs : Lista) -> {auto 0 _ : InBoundsnxs} -> a
Find a particular element of a list.

@ ok a proof that the index is within bounds
Totality: total
index' : (xs : Lista) -> Fin (lengthxs) -> a
Totality: total
init : (l : Lista) -> {auto 0 _ : NonEmptyl} -> Lista
Return all but the last element of a non-empty list.
@ ok proof the list is non-empty
Totality: total
init' : Lista -> Maybe (Lista)
Attempt to return all but the last element of a non-empty list.

If the list is empty, return `Nothing`.
Totality: total
inits : Lista -> List (Lista)
The inits function returns all initial segments of the argument, shortest
first. For example,

```idris example
inits [1,2,3]
```
Totality: total
intercalate : Lista -> List (Lista) -> Lista
Given a separator list and some more lists, produce a new list by
placing the separator between each of the lists.

@ sep the separator
@ xss the lists between which the separator will be placed

```idris example
intercalate [0, 0, 0] [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]
```
Totality: total
intersect : Eqa => Lista -> Lista -> Lista
Compute the intersect of two lists according to the `Eq` implementation for the elements.
Totality: total
intersectAll : Eqa => List (Lista) -> Lista
Totality: total
intersectAllBy : (a -> a -> Bool) -> List (Lista) -> Lista
Totality: total
intersectBy : (a -> a -> Bool) -> Lista -> Lista -> Lista
Compute the intersect of two lists by user-supplied equality predicate.
Totality: total
intersperse : a -> Lista -> Lista
Insert some separator between the elements of a list.

````idris example
with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
````

Totality: total
isCons : Lista -> Bool
Totality: total
isInfixOf : Eqa => Lista -> Lista -> Bool
The isInfixOf function takes two lists and returns True iff the first list
is contained, wholly and intact, anywhere within the second.

```idris example
isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
```
```idris example
isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
```

Totality: total
isNil : Lista -> Bool
Totality: total
isPrefixOf : Eqa => Lista -> Lista -> Bool
The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.
Totality: total
isPrefixOfBy : (a -> a -> Bool) -> Lista -> Lista -> Bool
Totality: total
isSuffixOf : Eqa => Lista -> Lista -> Bool
The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
Totality: total
isSuffixOfBy : (a -> a -> Bool) -> Lista -> Lista -> Bool
Totality: total
iterate : (a -> Maybea) -> a -> Lista
Generate a list by repeatedly applying a partial function until exhausted.
@ f the function to iterate
@ x the initial value that will be the head of the list
iterateN : Nat -> (a -> a) -> a -> Lista
Totality: total
last : (l : Lista) -> {auto 0 _ : NonEmptyl} -> a
Retrieve the last element of a non-empty list.
@ ok proof that the list is non-empty
Totality: total
last' : Lista -> Maybea
Attempt to retrieve the last element of a non-empty list.

If the list is empty, return `Nothing`.
Totality: total
lengthMap : (xs : Lista) -> length (mapfxs) = lengthxs
Totality: total
lookup : Eqa => a -> List (a, b) -> Maybeb
Find associated information in a list using Boolean equality.
Totality: total
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybeb
Find associated information in a list using a custom comparison.
Totality: total
mapMaybe : (a -> Maybeb) -> Lista -> Listb
Apply a partial function to the elements of a list, keeping the ones at which
it is defined.
Totality: total
merge : Orda => Lista -> Lista -> Lista
Merge two sorted lists using the default ordering for the type of their elements.
Totality: total
mergeBy : (a -> a -> Ordering) -> Lista -> Lista -> Lista
Merge two sorted lists using an arbitrary comparison
predicate. Note that the lists must have been sorted using this
Totality: total
mergeReplicate : a -> Lista -> Lista
Prefix every element in the list with the given element

```idris example
with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
```

Totality: total
nub : Eqa => Lista -> Lista
O(n^2). The nub function removes duplicate elements from a list. In
particular, it keeps only the first occurrence of each element. It is a
special case of nubBy, which allows the programmer to supply their own
equality test.

```idris example
nub (the (List _) [1,2,1,3])
```
Totality: total
nubBy : (a -> a -> Bool) -> Lista -> Lista
Totality: total
partition : (a -> Bool) -> Lista -> (Lista, Lista)
Totality: total
replaceOn : Eqa => a -> a -> Lista -> Lista
Replaces all occurences of the first argument with the second argument in a list.

```idris example
replaceOn '-' ',' ['1', '-', '2', '-', '3']
```

Totality: total
replaceWhen : (a -> Bool) -> a -> Lista -> Lista
Totality: total
replicate : Nat -> a -> Lista
Construct a list with `n` copies of `x`.
@ n how many copies
@ x the element to replicate
Totality: total
revAppend : (vs : Lista) -> (ns : Lista) -> reversens++reversevs = reverse (vs++ns)
Totality: total
reverse : Lista -> Lista
Totality: total
reverseInvolutive : (xs : Lista) -> reverse (reversexs) = xs
List reverse applied twice yields the identity function.
Totality: total
reverseOnto : Lista -> Lista -> Lista
Totality: total
snoc : Lista -> a -> Lista
Totality: total
sort : Orda => Lista -> Lista
Sort a list using the default ordering for the type of its elements.
Totality: total
sortBy : (a -> a -> Ordering) -> Lista -> Lista
Sort a list using some arbitrary comparison predicate.

@ cmp how to compare elements
@ xs the list to sort
Totality: total
sorted : Orda => Lista -> Bool
Check whether a list is sorted with respect to the default ordering for the type of its elements.
Totality: total
span : (a -> Bool) -> Lista -> (Lista, Lista)
Totality: total
spanBy : (a -> Maybeb) -> Lista -> (Listb, Lista)
Totality: total
split : (a -> Bool) -> Lista -> List1 (Lista)
Totality: total
splitAt : Nat -> Lista -> (Lista, Lista)
Totality: total
splitOn : Eqa => a -> Lista -> List1 (Lista)
Split on the given element.

```idris example
splitOn 0 [1,0,2,0,0,3]
```

Totality: total
tail : (l : Lista) -> {auto 0 _ : NonEmptyl} -> Lista
Get the tail of a non-empty list.
@ ok proof the list is non-empty
Totality: total
tail' : Lista -> Maybe (Lista)
Attempt to get the tail of a list. If the list is empty, return `Nothing`.
Totality: total
tails : Lista -> List (Lista)
The tails function returns all final segments of the argument, longest
first. For example,

```idris example
tails [1,2,3] == [[1,2,3], [2,3], , []]
```
Totality: total
take : Nat -> Lista -> Lista
Totality: total
takeWhile : (a -> Bool) -> Lista -> Lista
Totality: total
toList : Foldablet => ta -> Lista
Convert any Foldable structure to a list.
Totality: total
toList1 : (l : Lista) -> {auto 0 _ : NonEmptyl} -> List1a
Convert to a non-empty list.
@ ok proof the list is non-empty
Totality: total
toList1' : Lista -> Maybe (List1a)
Convert to a non-empty list, returning Nothing if the list is empty.
Totality: total
transpose : List (Lista) -> List (Lista)
Transposes rows and columns of a list of lists.

```idris example
with List transpose [[1, 2], [3, 4]]
```

This also works for non square scenarios, thus
involution does not always hold:

transpose [[], [1, 2]] = [, ]
transpose (transpose [[], [1, 2]]) = [[1, 2]]
Totality: total
unfoldr : (b -> Maybe (a, b)) -> b -> Lista
union : Eqa => Lista -> Lista -> Lista
Compute the union of two lists according to their `Eq` implementation.

```idris example
union ['d', 'o', 'g'] ['c', 'o', 'w']
```

Totality: total
unionBy : (a -> a -> Bool) -> Lista -> Lista -> Lista
The unionBy function returns the union of two lists by user-supplied equality predicate.
Totality: total