- zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) -> (z : List c) -> List d
Combine three lists elementwise using some function. If they are different

lengths, the result is truncated to the length of the shortest list.- f
the function to combine elements with

- x
the first list

- y
the second list

- z
the third list

- zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) -> List c
Combine two lists elementwise using some function. If they are different

lengths, the result is truncated to the length of the shorter list.- f
the function to combine elements with

- l
the first list

- r
the second list

- zip3 : (x : List a) -> (y : List b) -> (z : List c) -> List (a, b, c)
Combine three lists elementwise into tuples

- zip : (l : List a) -> (r : List b) -> List (a, b)
Combine two lists elementwise into pairs

- unzip3 : List (a, b, c) -> (List a, List b, List c)
Split a list of triples into three lists

- unzip : List (a, b) -> (List a, List b)
Split a list of pairs into two lists

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

- union : Eq a => List a -> List a -> List a
Compute the union of two lists according to their

`Eq`

implementation.`union ['d', 'o', 'g'] ['c', 'o', 'w']`

- transpose : List (List a) -> List (List a)
Transposes rows and columns of a list of lists.

`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]]TODO: Solution which satisfies the totality checker?

- toList : Foldable t => t a -> List a
Convert any Foldable structure to a list.

- takeWhile : (p : a -> Bool) -> List a -> List a
Take the longest prefix of a list such that all elements satisfy some

Boolean predicate.- p
the predicate

- take : (n : Nat) -> (xs : List a) -> List a
Take the first

`n`

elements of`xs`

If there are not enough elements, return the whole list.

- n
how many elements to take

- xs
the list to take them from

- tails : List a -> List (List a)
The tails function returns all final segments of the argument, longest

first. For example,`tails [1,2,3] == [[1,2,3], [2,3], [3], []]`

- tail' : (l : List a) -> Maybe (List a)
Attempt to get the tail of a list.

If the list is empty, return

`Nothing`

.- tail : (l : List a) -> {auto ok : NonEmpty l} -> List a
Get the tail of a non-empty list.

- ok
proof that the list is non-empty

- splitOn : Eq a => a -> List a -> List (List a)
Split on the given element.

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

- splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
A tuple where the first element is a List of the n first elements and

the second element is a List of the remaining elements of the list

It is equivalent to (take n xs, drop n xs)- n
the index to split at

- xs
the list to split in two

- split : (a -> Bool) -> List a -> List (List a)
Split on any elements that satisfy the given predicate.

`split (<2) [2,0,3,1,4]`

- span : (a -> Bool) -> List a -> (List a, List a)
Given a list and a predicate, returns a pair consisting of the longest

prefix of the list that satisfies a predicate and the rest of the list.`span (<3) [1,2,3,2,1]`

- sorted : Ord a => List a -> Bool
Check whether a list is sorted with respect to the default ordering for the type of its elements.

- sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
Sort a list using some arbitrary comparison predicate.

- cmp
how to compare elements

- xs
the list to sort

- sort : Ord a => List a -> List a
Sort a list using the default ordering for the type of its elements.

- scanl1 : (a -> a -> a) -> List a -> List a
The scanl1 function is a variant of scanl that doesn't require an explicit

starting value.

It assumes the first element of the list to be the starting value and then

starts the fold with the element following it.`scanl1 (+) [1,2,3,4]`

- scanl : (b -> a -> b) -> b -> List a -> List b
The scanl function is similar to foldl, but returns all the intermediate

accumulator states in the form of a list.`scanl (+) 0 [1,2,3,4]`

- reverse : List a -> List a
Return the elements of a list in reverse order.

- replicate : (n : Nat) -> (x : a) -> List a
Construct a list with

`n`

copies of`x`

- n
how many copies

- x
the element to replicate

- replaceOn : Eq a => a -> a -> List a -> List a
Replaces all occurences of the first argument with the second argument in a list.

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

- partition : (a -> Bool) -> List a -> (List a, List a)
The partition function takes a predicate a list and returns the pair of

lists of elements which do and do not satisfy the predicate, respectively;

e.g.,`partition (<3) [0, 1, 2, 3, 4, 5]`

- nubBy : (a -> a -> Bool) -> List a -> List a
The nubBy function behaves just like nub, except it uses a user-supplied

equality predicate instead of the overloaded == function.- 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.`nub (the (List _) [1,2,1,3])`

- nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
Decide whether a list is non-empty

- 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.- merge : Ord a => List a -> List a -> List a
Merge two sorted lists using the default ordering for the type of their elements.

- mapPreservesLength : (f : a -> b) -> (l : List a) -> length (map f l) = length l
Mapping a function over a list doesn't change its length.

- 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.- mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) -> map f (map g l) = map (f . g) l
Mapping two functions is the same as mapping their composition.

- mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) -> map f (l ++ r) = map f l ++ map f r
Mapping a function over two lists and appending them is equivalent

to appending them and then mapping the function.- lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
Find associated information in a list using a custom comparison.

- lookup : Eq a => a -> List (a, b) -> Maybe b
Find associated information in a list using Boolean equality.

- listToMaybe : List a -> Maybe a
Either return the head of a list, or

`Nothing`

if it is empty.- list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b
Simply-typed recursion operator for lists.

- nil
what to return at the end of the list

- cons
what to do at each step of recursion

- xs
the list to recurse over

- lengthAppend : (left : List a) -> (right : List a) -> length (left ++ right) = length left + length right
The length of two lists that are appended is the sum of the lengths

of the input lists.- length : List a -> Nat
Compute the length of a list.

Runs in linear time

- last' : (l : List a) -> Maybe a
Attempt to retrieve the last element of a non-empty list.

If the list is empty, return

`Nothing`

.- last : (l : List a) -> {auto ok : NonEmpty l} -> a
Retrieve the last element of a non-empty list.

- ok
proof that the list is non-empty

- isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
- 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.

- isPrefixOfBy : (eq : a -> a -> Bool) -> (left : List a) -> (right : List a) -> Bool
Check whether a list is a prefix of another according to a user-supplied equality test.

- eq
the equality comparison

- left
the potential prefix

- right
the list that may have

`left`

as its prefix

- 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.

- isNil : List a -> Bool
Returns

`True`

iff the argument is empty- 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.`isInfixOf ['b','c'] ['a', 'b', 'c', 'd']`

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

- isCons : List a -> Bool
Returns

`True`

iff the argument is not empty- intersperse : a -> List a -> List a
Insert some separator between the elements of a list.

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

- intercalate : (sep : List a) -> (xss : 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

- inits : List a -> List (List a)
The inits function returns all initial segments of the argument, shortest

first. For example,`inits [1,2,3]`

- init' : (l : List a) -> Maybe (List a)
Attempt to Return all but the last element of a list.

If the list is empty, return

`Nothing`

.- init : (l : List a) -> {auto ok : NonEmpty l} -> List a
Return all but the last element of a non-empty list.

- ok
proof that the list is non-empty

- index' : (n : Nat) -> (l : List a) -> Maybe a
Attempt to find a particular element of a list.

If the provided index is out of bounds, return Nothing.

- index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
Find a particular element of a list.

- ok
a proof that the index is within bounds

- inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
Decide whether

`k`

is a valid index into`xs`

- head' : (l : List a) -> Maybe a
Attempt to get the first element of a list. If the list is empty, return

`Nothing`

.- head : (l : List a) -> {auto ok : NonEmpty l} -> a
Get the first element of a non-empty list

- ok
proof that the list is non-empty

- hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
No list contains an element of the empty list.

- hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) -> hasAnyBy p [] l = False
No list contains an element of the empty list by any predicate.

- hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
Check if any elements of the first list are found in the second, using

a custom comparison.- hasAny : Eq a => List a -> List a -> Bool
Check if any elements of the first list are found in the second, using

Boolean equality.- foldlMatchesFoldr : (f : b -> a -> b) -> (q : b) -> (xs : List a) -> foldl f q xs = foldlAsFoldr f q xs
The definition of foldl works the same as the default definition

in terms of foldr- foldlAsFoldr : (b -> a -> b) -> b -> List a -> b
Implement foldl using foldr, for a later equality proof.

- findIndices : (a -> Bool) -> List a -> List Nat
Find the indices of all elements that satisfy some predicate.

- findIndex : (a -> Bool) -> List a -> Maybe Nat
Find the index of the first element of a list that satisfies a predicate, or

`Nothing`

if none do.- find : (a -> Bool) -> List a -> Maybe a
Find the first element of a list that satisfies a predicate, or

`Nothing`

if none do.- filterSmaller : (xs : List a) -> LTE (length (filter p xs)) (length xs)
A filtered list is no longer than its input

- filter : (a -> Bool) -> List a -> List a
filter, applied to a predicate and a list, returns the list of those

elements that satisfy the predicate; e.g.,`filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]`

- elemIndicesBy : (a -> a -> Bool) -> a -> List a -> List Nat
Find all indices for an element in a list, using a custom equality test.

- elemIndices : Eq a => a -> List a -> List Nat
Find all indices for an element in a list, using the default equality test for the type of list elements.

- elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat
Find the index of the first occurrence of an element in a list, using a custom equality test.

- elemIndex : Eq a => a -> List a -> Maybe Nat
Find the index of the first occurrence of an element in a list,

using the default equality test for the type of list elements.- elemBy : (a -> a -> Bool) -> a -> List a -> Bool
Check if something is a member of a list using a custom comparison.

- elem : Eq a => a -> List a -> Bool
Check if something is a member of a list using the default Boolean equality.

- dropWhile : (p : a -> Bool) -> List a -> List a
Remove the longest prefix of a list such that all removed elements satisfy some

Boolean predicate.- p
the predicate

- drop : (n : Nat) -> (xs : List a) -> List a
Drop the first

`n`

elements of`xs`

If there are not enough elements, return the empty list.

- n
how many elements to drop

- xs
the list to drop them from

- deleteBy : (a -> a -> Bool) -> a -> List a -> List a
The deleteBy function behaves like delete, but takes a user-supplied equality predicate.

- delete : Eq a => a -> List a -> List a
`delete x`

removes the first occurrence of`x`

from its list argument. For

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.- consInjective : (x :: xs = y :: ys) -> (x = y, xs = ys)
(::) is injective

- catMaybes : List (Maybe a) -> List a
Keep the

`Just`

elements in a list, discarding the`Nothing`

elements.- break : (a -> Bool) -> List a -> (List a, List a)
Given a list and a predicate, returns a pair consisting of the longest

prefix of the list that does not satisfy a predicate and the rest of the

list.`break (>=3) [1,2,3,2,1]`

- appendNilRightNeutral : (l : List a) -> l ++ [] = l
The empty list is a right identity for append.

- appendAssociative : (l : List a) -> (c : List a) -> (r : List a) -> l ++ c ++ r = (l ++ c) ++ r
Appending lists is associative.

- (\\) : Eq a => List a -> List a -> List a
The

`\\`

function is list difference (non-associative). In the result of

`xs \\ ys`

, the first occurrence of each element of ys in turn (if any) has

been removed from`xs`

, e.g.,`(([1,2] ++ [2,3]) \\ [1,2])`

- Fixity
- Non-associative, precedence 5

- data NonEmpty : (xs : List a) -> Type
Satisfiable if

`xs`

is non-empty (e.g., if`xs`

is a cons).- data List : (elem : Type) -> Type
Generic lists

- data InBounds : (k : Nat) -> (xs : 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

- (++) : List a -> List a -> List a
Append two lists

- Fixity
- Left associative, precedence 7