Prelude.List

zipWithTailProof : (a : Type) -> (b : Type) -> (c : Type) -> (f : a -> b -> c) -> (x : a) -> (xs : List a) -> (y : b) -> (ys : List b) -> (p : length (x :: xs) = length (y :: ys)) -> length xs = length ys

zipWith3TailProof' : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> (f : a -> b -> c -> d) -> (x : a) -> (xs : List a) -> (y : b) -> (ys : List b) -> (z : c) -> (zs : List c) -> (p : length (x :: xs) = length (y :: ys)) -> (q : length (y :: ys) = length (z :: zs)) -> length ys = length zs

zipWith3TailProof : (a : Type) -> (b : Type) -> (c : Type) -> (d : Type) -> (f : a -> b -> c -> d) -> (x : a) -> (xs : List a) -> (y : b) -> (ys : List b) -> (z : c) -> (zs : List c) -> (p : length (x :: xs) = length (y :: ys)) -> (q : length (y :: ys) = length (z :: zs)) -> length xs = length ys

zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) -> (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d

Combine three lists of the same length elementwise using some function.

f

the function to combine elements with

x

the first list

y

the second list

z

the third list

ok

a proof that the lengths of the first two inputs are equal

ok'

a proof that the lengths of the second and third inputs are equal

zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) -> (ok : length l = length r) -> List c

Combine two lists of the same length elementwise using some function.

f

the function to combine elements with

l

the first list

r

the second list

ok

a proof that the lengths of the inputs are equal

zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) -> (length y = length z) -> List (a, b, c)

Combine three lists elementwise into tuples

zip : (l : List a) -> (r : List b) -> (length l = length r) -> 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 instance.

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 : isCons l = True} -> 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

sort : Ord a => List a -> List a

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])

mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a

merge : Ord a => List a -> List a -> List a

mapPreservesLengthStepCase : (a : Type) -> (b : Type) -> (f : a -> b) -> (x : a) -> (xs : List a) -> (inductiveHypothesis : length (map f xs) = length xs) -> S (length (Prelude.List.List instance of Prelude.Functor.Functor, method map f xs)) = S (length xs)

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.

mapFusionStepCase : (b : Type) -> (c : Type) -> (f : b -> c) -> (a : Type) -> (g : a -> b) -> (x : a) -> (xs : List a) -> (inductiveHypothesis : map f (map g xs) = map (f . g) xs) -> f (g x) :: Prelude.List.List instance of Prelude.Functor.Functor, method map f (Prelude.List.List instance of Prelude.Functor.Functor, method map g xs) = f (g x) :: Prelude.List.List instance of Prelude.Functor.Functor, method map (\x1 => f (g x1)) xs

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.

mapDistributesOverAppendStepCase : (a : Type) -> (b : Type) -> (f : a -> b) -> (x : a) -> (xs : List a) -> (r : List a) -> (inductiveHypothesis : map f (xs ++ r) = map f xs ++ map f r) -> f x :: Prelude.List.List instance of Prelude.Functor.Functor, method map f (xs ++ r) = f x :: Prelude.List.List instance of Prelude.Functor.Functor, method map f xs ++ Prelude.List.List instance of Prelude.Functor.Functor, method map f r

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

lengthAppendStepCase : (a : Type) -> (x : a) -> (xs : List a) -> (right : List a) -> (inductiveHypothesis : length (xs ++ right) = length xs + length right) -> S (length (xs ++ right)) = S (plus (length xs) (length right))

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 : isCons l = True} -> 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 : (a -> a -> Bool) -> List a -> List a -> Bool

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

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 : isCons l = True} -> List a

Return all but the last element of a non-empty list.

ok

proof that the list is non-empty

indexTailProof : (a : Type) -> (n : Nat) -> (x : a) -> (xs : List a) -> (p : lt (S n) (length (x :: xs)) = True) -> lt n (length xs) = True

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) -> (l : List a) -> (ok : lt n (length l) = True) -> a

Find a particular element of a list.

ok

a proof that the index is within bounds

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 : isCons l = True} -> a

Get the first element of a non-empty list

ok

proof that the list is non-empty

hasAnyNilFalseBody : (a : Type) -> (l : List a) -> (constrarg : Eq a) -> hasAnyBy (==) [] l = False

hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False

No list contains an element of the empty list.

hasAnyByNilFalseStepCase : (a : Type) -> (p : a -> a -> Bool) -> (x : a) -> (xs : List a) -> (inductiveHypothesis : hasAnyBy p [] xs = False) -> hasAnyBy p [] xs = False

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

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.

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

elemIndices : Eq a => a -> List a -> List Nat

elemIndexBy : (a -> a -> Bool) -> a -> List a -> Maybe Nat

elemIndex : Eq a => a -> List a -> Maybe Nat

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.

catMaybes : List (Maybe a) -> List a

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]

appendNilRightNeutralStepCase : (a : Type) -> (x : a) -> (xs : List a) -> (inductiveHypothesis : xs ++ [] = xs) -> x :: xs ++ [] = x :: xs

appendNilRightNeutral : (l : List a) -> l ++ [] = l

The empty list is a right identity for append.

appendAssociativeStepCase : (a : Type) -> (x : a) -> (xs : List a) -> (c : List a) -> (r : List a) -> (inductiveHypothesis : xs ++ c ++ r = (xs ++ c) ++ r) -> x :: xs ++ c ++ r = x :: (xs ++ c) ++ r

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 List : Type -> Type

Linked lists

Nil : List a

The empty list

(::) : a -> List a -> List a

Cons cell

Fixity

Left associative, precedence 7

(++) : List a -> List a -> List a

Append two lists

Fixity

Left associative, precedence 7