stdlib - 0.0.1

Stdlib.Data.List.Base

Definitions

builtin list type List (a : Type)Source#

Inductive list.

Constructors

| nil

The empty list

| :: a (List a)

An element followed by a list

elem {A} (eq : A A Bool) (s : A) : List A BoolSource#

𝒪(𝓃). Returns true if the given object is in the List.

foldr {A B} (f : A B B) (z : B) : List A BSource#

Right-associative fold.

rfor {A B} (f : B A B) (acc : B) : List A BSource#

foldl {A B} (f : B A B) (z : B) : List A BSource#

Left-associative and tail-recursive fold.

for : {A B : Type} (B A B) B List A BSource#

map {A B} (f : A B) : List A List BSource#

𝒪(𝓃). Maps a function over each element of a List.

filter {A} (f : A Bool) : List A List ASource#

𝒪(𝓃). Filters a List according to a given predicate, i.e., keeps the elements for which the given predicate returns true.

length {A} (l : List A) : NatSource#

𝒪(𝓃). Returns the length of the List.

reverse {A} (l : List A) : List ASource#

𝒪(𝓃). Returns the given List in reverse order.

replicate {A} : Nat A List ASource#

Returns a List of length n where every element is the given value.

take {A} : Nat List A List ASource#

Takes the first n elements of a List.

drop {A} : Nat List A List ASource#

Drops the first n elements of a List.

splitAt {A} : Nat List A List A × List ASource#

𝒪(𝓃). splitAt n xs returns a tuple where first element is xs prefix of length n and second element is the remainder of the List.

terminating merge {A} {{Ord A}} : List A List A List ASource#

𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.

partition {A} (f : A Bool) : List A List A × List ASource#

𝒪(𝓃). Returns a tuple where the first component has the items that satisfy the predicate and the second component has the elements that don't.

++ : {A : Type} List A List A List ASource#

Concatenates two Lists.

snoc {A} (xs : List A) (x : A) : List ASource#

𝒪(𝓃). Append an element.

flatten : {A : Type} List (List A) List ASource#

Concatenates a List of Lists.

prependToAll {A} (sep : A) : List A List ASource#

𝒪(𝓃). Inserts the given element before every element in the given List.

intersperse {A} (sep : A) : List A List ASource#

𝒪(𝓃). Inserts the given element inbetween every two elements in the given List.

tail {A} : List A List ASource#

𝒪(1). Drops the first element of a List.

any {A} (f : A Bool) : List A BoolSource#

𝒪(𝓃). Returns true if at least one element of the List satisfies the predicate.

all {A} (f : A -> Bool) : List A -> BoolSource#

𝒪(𝓃). Returns true if all elements of the List satisfy the predicate.

null {A} : List A BoolSource#

𝒪(1). Returns true if the List is empty.

zipWith {A B C} (f : A -> B -> C) : List A -> List B -> List CSource#

𝒪(min(𝓂, 𝓃)). Returns a list containing the results of applying a function to each pair of elements from the input lists.

zip {A B} : List A -> List B -> List (A × B)Source#

𝒪(min(𝓂, 𝓃)). Returns a list of pairs formed from the input lists.

mergeSort {A} {{Ord A}} (l : List A) : List ASource#

𝒪(𝓃 log 𝓃). Sorts a list of elements in ascending order using the MergeSort algorithm.

terminating quickSort {A} {{Ord A}} : List A List ASource#

On average 𝒪(𝓃 log 𝓃), worst case 𝒪(𝓃²). Sorts a list of elements in ascending order using the QuickSort algorithm.

catMaybes {A} : List (Maybe A) -> List ASource#

𝒪(𝓃) Filters out every nothing from a List.

concatMap {A B} (f : A -> List B) : List A -> List BSource#

Applies a function to every item on a List and concatenates the result. 𝒪(𝓃), where 𝓃 is the number of items in the resulting list.

transpose {A} : List (List A) -> List (List A)Source#

𝒪(𝓃 * 𝓂). Transposes a List of Lists interpreted as a matrix.