Stdlib.Data.List

Contents

Inductive list.

Constructors

\| nil : List a	The empty list
\| :: : a → List a → List a	An element followed by a list

elem : {A : Type} → (A → A → Bool) → A → List A → BoolSource #

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

foldr : {A : Type} → {B : Type} → (A → B → B) → B → List A → BSource #

Right-associative fold.

foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → BSource #

Left-associative and tail-recursive fold.

map : {A : Type} → {B : Type} → (A → B) → List A → List BSource #

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

filter : {A : Type} → (A → Bool) → List A → List ASource #

𝒪(𝓃). Only keeps the elements for which the given predicate returns true.

length : {A : Type} → List A → NatSource #

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

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

replicate : {A : Type} → Nat → A → List ASource #

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

take : {A : Type} → Nat → List A → List ASource #

Takes the first n elements of a List.

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

merge : {A : Type} → (A → A → Ordering) → List A → List A → List ASource #

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

partition : {A : Type} → (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.

Concatenates a List of Lists.

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

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

head : {A : Type} → List A → ASource #

𝒪(1). Partial function that returns the first element of a List.

tail : {A : Type} → List A → List ASource #

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

terminating transpose : {A : Type} → List (List A) → List (List A)Source #

𝒪(𝓃 * 𝓂). Partial function that transposes a List of Lists interpreted as a matrix.

any : {A : Type} → (A → Bool) → List A → BoolSource #

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

null : {A : Type} → List A → BoolSource #

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

Description

Definitions