- data InBounds : Nat -> List a -> 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 : InBounds 0 (x :: xs)
Z is a valid index into any cons cell
- InLater : InBounds k xs -> InBounds (S k) (x :: xs)
Valid indices can be extended
- data NonEmpty : List a -> Type
- Totality: total
Constructor: - IsNonEmpty : NonEmpty (x :: xs)
- (\\) : Eq a => List a -> List a -> List a
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 : List a) -> (c : List a) -> (r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
Appending lists is associative.
Totality: total- appendNilRightNeutral : (l : List a) -> l ++ [] = l
The empty list is a right identity for append.
Totality: total- break : (a -> Bool) -> List a -> (List a, List a)
- Totality: total
- catMaybes : List (Maybe a) -> List a
Extract all of the values contained in a List of Maybes
Totality: total- consInjective : the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)
(::) is injective
Totality: total- delete : Eq a => a -> List a -> List a
`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 -> List a -> List a
The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
Totality: total- deleteFirstsBy : (a -> a -> Bool) -> List a -> List a -> List a
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 -> List a -> List a
- Totality: total
- dropFusion : (n : Nat) -> (m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n + m) l
- Totality: total
- dropWhile : (a -> Bool) -> List a -> List a
- Totality: total
- elemBy : (a -> a -> Bool) -> a -> List a -> Bool
Check if something is a member of a list using a custom comparison.
Totality: total- filter : (a -> Bool) -> List a -> List a
Applied to a predicate and a list, returns the list of those elements that
satisfy the predicate.
Totality: total- find : (a -> Bool) -> List a -> Maybe a
Find the first element of the list that satisfies the predicate.
Totality: total- findIndex : (a -> Bool) -> (xs : List a) -> Maybe (Fin (length xs))
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) -> List a -> List Nat
Find indices of all elements that satisfy the given test.
Totality: total- foldl1 : (a -> a -> a) -> (l : List a) -> {auto 0 _ : NonEmpty l} -> 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 : List a) -> {auto 0 _ : NonEmpty l} -> b
- Totality: total
- foldr1 : (a -> a -> a) -> (l : List a) -> {auto 0 _ : NonEmpty l} -> 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 : List a) -> {auto 0 _ : NonEmpty l} -> b
- Totality: total
- group : Eq a => List a -> List (List1 a)
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 : Ord b => (a -> b) -> List a -> List (List1 a)
`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) -> List a -> List (List1 a)
`groupBy` operates like `group`, but uses the provided equality
predicate instead of `==`.
Totality: total- groupWith : Eq b => (a -> b) -> List a -> List (List1 a)
`groupWith` operates like `group`, but uses the provided projection when
comparing for equality
Totality: total- head : (l : List a) -> {auto 0 _ : NonEmpty l} -> a
Get the head of a non-empty list.
@ ok proof the list is non-empty
Totality: total- head' : List a -> Maybe a
Attempt to get the head of a list. If the list is empty, return `Nothing`.
Totality: total- inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
Decide whether `k` is a valid index into `xs`.
Totality: total- index : (n : Nat) -> (xs : List a) -> {auto 0 _ : InBounds n xs} -> a
Find a particular element of a list.
@ ok a proof that the index is within bounds
Totality: total- index' : (xs : List a) -> Fin (length xs) -> a
- Totality: total
- init : (l : List a) -> {auto 0 _ : NonEmpty l} -> List a
Return all but the last element of a non-empty list.
@ ok proof the list is non-empty
Totality: total- init' : List a -> Maybe (List a)
Attempt to return all but the last element of a non-empty list.
If the list is empty, return `Nothing`.
Totality: total- inits : List a -> List (List a)
The inits function returns all initial segments of the argument, shortest
first. For example,
```idris example
inits [1,2,3]
```
Totality: total- intercalate : List a -> List (List a) -> List a
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 : Eq a => List a -> List a -> List a
Compute the intersect of two lists according to the `Eq` implementation for the elements.
Totality: total- intersectAll : Eq a => List (List a) -> List a
- Totality: total
- intersectAllBy : (a -> a -> Bool) -> List (List a) -> List a
- Totality: total
- intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
Compute the intersect of two lists by user-supplied equality predicate.
Totality: total- intersperse : a -> List a -> List a
Insert some separator between the elements of a list.
````idris example
with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
````
Totality: total- isCons : List a -> Bool
- Totality: total
- isInfixOf : Eq a => List a -> List a -> 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 : List a -> Bool
- Totality: total
- isPrefixOf : Eq a => List a -> List a -> 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) -> List a -> List a -> Bool
- Totality: total
- isSuffixOf : Eq a => List a -> List a -> 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) -> List a -> List a -> Bool
- Totality: total
- iterate : (a -> Maybe a) -> a -> List a
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 -> List a
- Totality: total
- last : (l : List a) -> {auto 0 _ : NonEmpty l} -> a
Retrieve the last element of a non-empty list.
@ ok proof that the list is non-empty
Totality: total- last' : List a -> Maybe a
Attempt to retrieve the last element of a non-empty list.
If the list is empty, return `Nothing`.
Totality: total- lengthMap : (xs : List a) -> length (map f xs) = length xs
- Totality: total
- lookup : Eq a => a -> List (a, b) -> Maybe b
Find associated information in a list using Boolean equality.
Totality: total- lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
Find associated information in a list using a custom comparison.
Totality: total- mapMaybe : (a -> Maybe b) -> List a -> List b
Apply a partial function to the elements of a list, keeping the ones at which
it is defined.
Totality: total- merge : Ord a => List a -> List a -> List a
Merge two sorted lists using the default ordering for the type of their elements.
Totality: total- mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
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 -> List a -> List a
Prefix every element in the list with the given element
```idris example
with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
```
Totality: total- nub : Eq a => List a -> List a
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) -> List a -> List a
- Totality: total
- partition : (a -> Bool) -> List a -> (List a, List a)
- Totality: total
- replaceOn : Eq a => a -> a -> List a -> List a
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 -> List a -> List a
- Totality: total
- replicate : Nat -> a -> List a
Construct a list with `n` copies of `x`.
@ n how many copies
@ x the element to replicate
Totality: total- revAppend : (vs : List a) -> (ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
- Totality: total
- reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
List reverse applied twice yields the identity function.
Totality: total- snoc : List a -> a -> List a
- Totality: total
- sort : Ord a => List a -> List a
Sort a list using the default ordering for the type of its elements.
Totality: total- sortBy : (a -> a -> Ordering) -> List a -> List a
Sort a list using some arbitrary comparison predicate.
@ cmp how to compare elements
@ xs the list to sort
Totality: total- sorted : Ord a => List a -> Bool
Check whether a list is sorted with respect to the default ordering for the type of its elements.
Totality: total- span : (a -> Bool) -> List a -> (List a, List a)
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 -> Maybe b) -> List a -> (List b, List a)
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) -> List a -> List1 (List a)
- Totality: total
- splitAt : Nat -> List a -> (List a, List a)
- Totality: total
- splitOn : Eq a => a -> List a -> List1 (List a)
Split on the given element.
```idris example
splitOn 0 [1,0,2,0,0,3]
```
Totality: total- tail : (l : List a) -> {auto 0 _ : NonEmpty l} -> List a
Get the tail of a non-empty list.
@ ok proof the list is non-empty
Totality: total- tail' : List a -> Maybe (List a)
Attempt to get the tail of a list. If the list is empty, return `Nothing`.
Totality: total- tails : List a -> List (List a)
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 -> List a -> List a
- Totality: total
- takeWhile : (a -> Bool) -> List a -> List a
- Totality: total
- toList1 : (l : List a) -> {auto 0 _ : NonEmpty l} -> List1 a
Convert to a non-empty list.
@ ok proof the list is non-empty
Totality: total- toList1' : List a -> Maybe (List1 a)
Convert to a non-empty list, returning Nothing if the list is empty.
Totality: total- transpose : List (List a) -> List (List a)
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 -> List a
-
- union : Eq a => List a -> List a -> List a
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) -> List a -> List a -> List a
The unionBy function returns the union of two lists by user-supplied equality predicate.
Totality: total