Data.List

Reexports

import public Control.Function
import public Data.Zippable

Definitions

isNil : List a -> Bool

  Boolean check for whether the list is the empty list.

Totality: total
Visibility: public export

isCons : List a -> Bool

  Boolean check for whether the list contains a cons (::) / is non-empty.

Totality: total
Visibility: public export

snoc : List a -> a -> List a

  Add an element to the end of a list.
  O(n). See the `Data.SnocList` module if you need to perform `snoc` often.

Totality: total
Visibility: public export

take : Nat -> List a -> List a

  Take `n` first elements from `xs`, returning the whole list if
  `n` >= length `xs`.
  
  @ n  the number of elements to take
  @ xs the list to take the elements from

Totality: total
Visibility: public export

drop : Nat -> List a -> List a

  Remove `n` first elements from `xs`, returning the empty list if
  `n >= length xs`
  
  @ n  the number of elements to remove
  @ xs the list to drop the elements from

Totality: total
Visibility: public export

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
Visibility: public export
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

Hints:

Uninhabited (InBounds k [])
Uninhabited (InBounds k xs) => Uninhabited (InBounds (S k) (x :: xs))

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

  Decide whether `k` is a valid index into `xs`.

Totality: total
Visibility: public export

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
Visibility: public export

index' : (xs : List a) -> Fin (length xs) -> a

Totality: total
Visibility: public export

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

Visibility: public export

unfoldr : (b -> Maybe (a, b)) -> b -> List a

  Given a function `f` which extracts an element of `b` and `b`'s
  continuation, return the list consisting of the extracted elements.
  CAUTION: Only terminates if `f` eventually returns `Nothing`.
  
  @ f  a function which provides an element of `b` and the rest of `b`
  @ b  a structure contanining any number of elements

Visibility: public export

iterateN : Nat -> (a -> a) -> a -> List a

  Returns the list of elements obtained by applying `f` to `x` `0` to `n-1` times,
  starting with `x`.
  
  @ n  the number of times to iterate `f` over `x`
  @ f  a function producing a series
  @ x  the initial element of the series

Totality: total
Visibility: public export

takeWhile : (a -> Bool) -> List a -> List a

  Get the longest prefix of the list that satisfies the predicate.
  
  @ p  a custom predicate for the elements of the list
  @ xs the list of elements

Totality: total
Visibility: public export

dropWhile : (a -> Bool) -> List a -> List a

  Remove elements from the list until an element no longer satisfies the
  predicate.
  
  @ p  a custom predicate for the elements of the list
  @ xs the list of elements to remove from

Totality: total
Visibility: public export

find : (a -> Bool) -> List a -> Maybe a

  Find the first element of the list that satisfies the predicate.

Totality: total
Visibility: public export

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
Visibility: public export

findIndices : (a -> Bool) -> List a -> List Nat

  Find indices of all elements that satisfy the given test.

Totality: total
Visibility: public export

lookupBy : (a -> b -> Bool) -> a -> List (b, v) -> Maybe v

  Find associated information in a list using a custom comparison.

Totality: total
Visibility: public export

lookup : Eq a => a -> List (a, b) -> Maybe b

  Find associated information in a list using Boolean equality.

Totality: total
Visibility: public export

nubBy : (a -> a -> Bool) -> List a -> List a

  Remove duplicate elements from a list using a custom comparison. The general
  case of `nub`.
  O(n^2).
  
  @ p  a custom comparison for detecting duplicate elements
  @ xs the list to remove the duplicates from

Totality: total
Visibility: public export

nub : Eq a => List a -> List a

  The nub function removes duplicate elements from a list using
  boolean equality. 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.
  O(n^2).
  
  ```idris example
  nub (the (List _) [1,2,1,3])
  ```

Totality: total
Visibility: public export

insertAt : (idx : Nat) -> a -> (xs : List a) -> {auto 0 _ : LTE idx (length xs)} -> List a

  Insert an element at a particular index.
  
  ```idris example
  insertAt 1 [6, 8, 9] 7
  ```
  
  @idx The index of the inserted value in the resulting list.
  @x The value to insert.
  @xs The list to insert the value into.

Totality: total
Visibility: public export

deleteAt : (idx : Nat) -> (xs : List a) -> {auto 0 _ : InBounds idx xs} -> List a

  Construct a new list consisting of all but the indicated element.
  
  ```idris example
  deleteAt 3 [5, 6, 7, 8, 9]
  ```
  
  @ idx The index of the value to delete.
  @ xs The list to delete the value from.

Totality: total
Visibility: public export

deleteBy : (a -> b -> Bool) -> a -> List b -> List b

  The deleteBy function behaves like delete, but takes a user-supplied equality predicate.

Totality: total
Visibility: public export

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
Visibility: public export

deleteFirstsBy : (a -> b -> Bool) -> List b -> List a -> List b

  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
Visibility: public export

(\\) : 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
Visibility: public export
Fixity Declaration: infix operator, level 7

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

break : (a -> Bool) -> List a -> (List a, List a)

  Similar to `span` but negates the predicate, i.e.: returns a tuple
  consisting of the longest prefix of the list whose elements don't satisfy
  the predicate, and the rest of the list.

Totality: total
Visibility: public export

singleton : a -> List a

Totality: total
Visibility: public export

split : (a -> Bool) -> List a -> List1 (List a)

Totality: total
Visibility: public export

splitAt : Nat -> List a -> (List a, List a)

  Split the list `xs` at the index `n`. If `n > length xs`, returns a tuple
  consisting of `xs` and `[]`.
  
  @ n  the index to split the list at
  @ xs the list to split

Totality: total
Visibility: public export

partition : (a -> Bool) -> List a -> (List a, List a)

  Divide the list into a tuple containing two smaller lists: one with the
  elements that satisfies the given predicate and another with the elements
  that don't.
  
  @ p  the predicate to partition according to
  @ xs the list to partition

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

replaceAt : (idx : Nat) -> a -> (xs : List a) -> {auto 0 _ : InBounds idx xs} -> List a

  Replace an element at a particlar index with another.
  
  ```idris example
  replaceAt 2 6 [1, 2, 3, 4]
  ```
  
  @idx The index of the value to replace.
  @x The value to insert.
  @xs The list in which to replace an element.

Totality: total
Visibility: public export

replaceWhen : (a -> Bool) -> a -> List a -> List a

  Replace the elements in the list that satisfy the predicate with the given
  value. The general case of `replaceOn`.
  
  @ p  the predicate to replace elements in the list according to
  @ b  the element to replace with
  @ l  the list to perform the replacements on

Totality: total
Visibility: public export

replaceOn : Eq a => a -> a -> List a -> List a

  Replace the elements in the list that are equal to `e`, using boolean
  equality, with `b`. A special case of `replaceWhen`, using `== e` as the
  predicate.
  
  ```idris example
  > replaceOn '-' ',' ['1', '-', '2', '-', '3']
  ['1', ',', '2', ',', '3']
  ```
  
  @ e  the element to find and replace
  @ b  the element to replace with
  @ l  the list to perform the replacements on

Totality: total
Visibility: public export

replicate : Nat -> a -> List a

  Construct a list with `n` copies of `x`.
  
  @ n how many copies
  @ x the element to replicate

Totality: total
Visibility: public export

intersectBy : (a -> a -> Bool) -> List a -> List a -> List a

  Compute the intersect of two lists by user-supplied equality predicate.

Totality: total
Visibility: export

intersect : Eq a => List a -> List a -> List a

  Compute the intersection of two lists according to the `Eq` implementation for
  the elements.

Totality: total
Visibility: export

intersectAllBy : (a -> a -> Bool) -> List (List a) -> List a

  Compute the intersect of all the lists in the given list of lists, according
  to the user-supplied equality predicate.
  
  @ eq the predicate for computing the intersection
  @ ls the list of lists to compute the intersect of

Totality: total
Visibility: export

intersectAll : Eq a => List (List a) -> List a

  Compute the intersect of all the lists in the given list of lists, according
  to boolean equality. A special case of `intersectAllBy`, using `==` as the
  equality predicate.
  
  @ ls the list of lists to compute the intersect of

Totality: total
Visibility: export

data NonEmpty : List a -> Type

  Proof that a given list is non-empty.

Totality: total
Visibility: public export
Constructor:

IsNonEmpty : NonEmpty (x :: xs)

Hint:

Uninhabited (NonEmpty [])

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

minimum : Ord a => (xs : List a) -> {auto 0 _ : NonEmpty xs} -> a

  Computes the minimum of a non-empty list

Totality: total
Visibility: public export

uncons' : List a -> Maybe (a, List a)

  Attempt to deconstruct the list into a head and a tail.

Totality: total
Visibility: public export

head' : List a -> Maybe a

  Attempt to get the head of a list. If the list is empty, return `Nothing`.

Totality: total
Visibility: public export

tail' : List a -> Maybe (List a)

  Attempt to get the tail of a list. If the list is empty, return `Nothing`.

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

foldr1By : (a -> b -> b) -> (a -> b) -> (l : List a) -> {auto 0 _ : NonEmpty l} -> b

  Foldr a non-empty list, using `map` to transform the first accumulated
  element to something of the desired type and `func` to accumulate the
  elements.
  
  @ func the function used to accumulate the elements
  @ map  an initial transformation from the element to the accumulated type
  @ l    the non-empty list to foldr
  @ ok   proof that the list is non-empty

Totality: total
Visibility: public export

foldl1By : (b -> a -> b) -> (a -> b) -> (l : List a) -> {auto 0 _ : NonEmpty l} -> b

  Foldl a non-empty list, using `map` to transform the first accumulated
  element to something of the desired type and `func` to accumulate the
  elements.
  
  @ func the function used to accumulate the elements
  @ map  an initial transformation from the element to the accumulated type
  @ l    the non-empty list to foldl
  @ ok   proof that the list is non-empty

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: export

toList1' : List a -> Maybe (List1 a)

  Convert to a non-empty list, returning Nothing if the list is empty.

Totality: total
Visibility: public export

interleave : List a -> List a -> List a

  Interleave two lists.
  ```idris example
  > interleave ["a", "c", "e"]  ["b", "d", "f"]
  ["a", "b", "c", "d", "e", "f"]
  ```

Totality: total
Visibility: public export

mergeReplicate : a -> List a -> List a

  Prefix every element in the list with the given element.
  
  @ sep the value to prefix
  @ xs  the list of elements to prefix with the given element
  
  ```idris example
  > with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
  ['>', 'a', '>', 'b', '>', 'c', '>', 'd', '>', 'e']
  ```

Totality: total
Visibility: public export

intersperse : a -> List a -> List a

  Insert some separator between the elements of a list.
  
  @ sep the value to intersperse
  @ xs  the list of elements to intersperse with the separator
  
  ```idris example
  > with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
  ['a', ',', 'b', ',', 'c', ',', 'd', ',', 'e']
  ```

Totality: total
Visibility: public export

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
Visibility: export

catMaybes : List (Maybe a) -> List a

  Extract all of the values contained in a List of Maybes

Totality: total
Visibility: public export

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
Visibility: export

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
Visibility: export

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
Visibility: export

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
Visibility: export

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

  Sort a list using the default ordering for the type of its elements.

Totality: total
Visibility: export

prefixOfBy : (a -> b -> Maybe m) -> List a -> List b -> Maybe (List m, List b)

  Check whether the `left` list is a prefix of the `right` one, according to
  `match`. Returns the matched prefix together with the leftover suffix.
  
  @ match a custom matching function for checking the elements are convertible
  @ left  the list which might be a prefix of `right`
  @ right the list of elements to compare against

Totality: total
Visibility: public export

isPrefixOfBy : (a -> b -> Bool) -> List a -> List b -> Bool

  Check whether the `left` list is a prefix of the `right` one, using the
  provided equality function to compare elements.
  
  @ eq    a custom equality function for comparing the elements
  @ left  the list which might be a prefix of `right`
  @ right the list of elements to compare againts

Totality: total
Visibility: public export

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 when comparing elements using `==`.

Totality: total
Visibility: public export

suffixOfBy : (a -> b -> Maybe m) -> List a -> List b -> Maybe (List b, List m)

  Check whether the `left` is a suffix of the `right` one, according to
  `match`. Returns the matched suffix together with the leftover prefix.
  
  @ match a custom matching function for checking the elements are convertible
  @ left  the list which might be a prefix of `right`
  @ right the list of elements to compare against

Totality: total
Visibility: public export

isSuffixOfBy : (a -> b -> Bool) -> List a -> List b -> Bool

  Check whether the `left` is a suffix of the `right` one, using the provided
  equality function to compare elements.
  
  @ eq    a custom equality function for comparing the elements
  @ left  the list which might be a suffix of `right`
  @ right the list of elements to compare againts

Totality: total
Visibility: public export

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 when comparing elements using `==`.

Totality: total
Visibility: public export

infixOfBy : (a -> b -> Maybe m) -> List a -> List b -> Maybe (List b, (List m, List b))

  Check whether the `left` list is an infix of the `right` one, according to
  `match`. Returns the shortest unmatched prefix, matched infix and the leftover suffix.

Totality: total
Visibility: public export

isInfixOfBy : (a -> b -> Bool) -> List a -> List b -> Bool

  Check whether the `left` is an infix of the `right` one, using the provided
  equality function to compare elements.

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: export

groupBy : (a -> a -> Bool) -> List a -> List (List1 a)

  `groupBy` operates like `group`, but uses the provided equality
  predicate instead of `==`.

Totality: total
Visibility: public export

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
Visibility: public export

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
Visibility: public export

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
Visibility: public export

grouped : (n : Nat) -> {auto 0 _ : IsSucc n} -> List a -> List (List a)

  Partitions a list into fixed sized sublists.
  
  Note: The last list in the result might be shorter than the rest if
        the input cannot evenly be split into groups of the same size.
  
  ```idris example
  grouped 3 [1..10] === [[1,2,3],[4,5,6],[7,8,9],[10]]
  ```

Totality: total
Visibility: public export

consInjective : the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)

  Heterogeneous injectivity for (::)

Totality: total
Visibility: export

reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs

  List `reverse` applied twice yields the identity function.

Totality: total
Visibility: export

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

  The empty list is a right identity for append.

Totality: total
Visibility: export

appendAssociative : (l : List a) -> (c : List a) -> (r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r

  Appending lists is associative.

Totality: total
Visibility: export

revAppend : (vs : List a) -> (ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)

  `reverse` is distributive

Totality: total
Visibility: export

dropFusion : (n : Nat) -> (m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n + m) l

  Dropping `m` elements from `l` and then dropping `n` elements from the
  result, is the same as simply dropping `n+m` elements from `l`

Totality: total
Visibility: export

lengthMap : (xs : List a) -> length (map f xs) = length xs

  Mapping a function over a list does not change the length of the list.

Totality: total
Visibility: export

lengthReplicate : (n : Nat) -> length (replicate n x) = n

  Proof that replicate produces a list of the requested length.

Totality: total
Visibility: export

foldlAppend : (f : (acc -> a -> acc)) -> (init : acc) -> (xs : List a) -> (ys : List a) -> foldl f init (xs ++ ys) = foldl f (foldl f init xs) ys

Totality: total
Visibility: export

filterAppend : (f : (a -> Bool)) -> (xs : List a) -> (ys : List a) -> filter f (xs ++ ys) = filter f xs ++ filter f ys

Totality: total
Visibility: export

mapMaybeFusion : (g : (b -> Maybe c)) -> (f : (a -> Maybe b)) -> (xs : List a) -> mapMaybe g (mapMaybe f xs) = mapMaybe (f >=> g) xs

Totality: total
Visibility: export

mapMaybeAppend : (f : (a -> Maybe b)) -> (xs : List a) -> (ys : List a) -> mapMaybe f (xs ++ ys) = mapMaybe f xs ++ mapMaybe f ys

Totality: total
Visibility: export

mapFusion : (g : (b -> c)) -> (f : (a -> b)) -> (xs : List a) -> map g (map f xs) = map (g . f) xs

Totality: total
Visibility: export

mapAppend : (f : (a -> b)) -> (xs : List a) -> (ys : List a) -> map f (xs ++ ys) = map f xs ++ map f ys

Totality: total
Visibility: export