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

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]] = [, ]  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