Idris2Doc : Data.List

Data.List

dataInBounds : 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 : InBounds0 (x::xs)
  Z is a valid index into any cons cell
InLater : InBoundskxs -> InBounds (Sk) (x::xs)
  Valid indices can be extended
dataNonEmpty : Lista -> Type
Totality: total
Constructor: 
IsNonEmpty : NonEmpty (x::xs)
(\\) : Eqa => Lista -> Lista -> Lista
  The non-associative list-difference.
A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@
interface.
Deletes the first occurrence of each element of the second list from the first list.

In the following example, the result is `[2, 4]`.
```idris example
[1, 2, 3, 4] // [1, 3]
```

Totality: total
Fixity Declaration: infix operator, level 7
appendAssociative : (l : Lista) -> (c : Lista) -> (r : Lista) -> l++ (c++r) = (l++c) ++r
  Appending lists is associative.

Totality: total
appendNilRightNeutral : (l : Lista) -> l++ [] = 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
deleteFirstsBy : (a -> a -> Bool) -> Lista -> Lista -> Lista
  Delete the first occurrence of each element from the second list in the first
list where equality is determined by the predicate passed as the first argument.
@ p A function that returns true when its two arguments should be considered equal.
@ source The list to delete elements from.
@ undesirables The list of elements to delete.

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
  Applied to a predicate and a list, returns the list of those elements that
satisfy the predicate.

Totality: total
find : (a -> Bool) -> Lista -> Maybea
  Find the first element of the list that satisfies the predicate.

Totality: total
findIndex : (a -> Bool) -> (xs : Lista) -> Maybe (Fin (lengthxs))
  Find the index and proof of InBounds of the first element (if exists) of a
list that satisfies the given test, else `Nothing`.

Totality: total
findIndices : (a -> Bool) -> Lista -> ListNat
  Find indices of all elements that satisfy the given test.

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
group : Eqa => Lista -> List (List1a)
  The `group` function takes a list of values and returns a list of
lists such that flattening the resulting list is equal to the
argument. Moreover, each list in the resulting list
contains only equal elements.

Totality: total
groupAllWith : Ordb => (a -> b) -> Lista -> List (List1a)
  `groupAllWith` operates like `groupWith`, but sorts the list
first so that each equivalence class has, at most, one list in the
output

Totality: total
groupBy : (a -> a -> Bool) -> Lista -> List (List1a)
  `groupBy` operates like `group`, but uses the provided equality
predicate instead of `==`.

Totality: total
groupWith : Eqb => (a -> b) -> Lista -> List (List1a)
  `groupWith` operates like `group`, but uses the provided projection when
comparing for equality

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
head' : Lista -> Maybea
  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
predicate already.

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
reverseInvolutive : (xs : Lista) -> reverse (reversexs) = xs
  List reverse applied twice yields the identity function.

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)
  Given a predicate and a list, returns a tuple consisting of the longest
prefix of the list whose elements satisfy the predicate, and the rest of the
list.

Totality: total
spanBy : (a -> Maybeb) -> Lista -> (Listb, Lista)
  Like @span@ but using a predicate that might convert a to b, i.e. given a
predicate from a to Maybe b and a list of as, returns a tuple consisting of
the longest prefix of the list where a -> Just b, and the rest of the list.

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], [3], []]
```

Totality: total
take : Nat -> Lista -> Lista
Totality: total
takeWhile : (a -> Bool) -> Lista -> Lista
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]] = [[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