Hanoi - 0.1.0

Stdlib.Data.List.Base

Definitions

type List (a : Type)Source#

Inductive list.

Constructors

| nil : List a

The empty list

| :: : aList aList a

An element followed by a list

elem : {A : Type}(AABool)AList ABoolSource#

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

foldr : {A : Type}{B : Type}(ABB)BList ABSource#

Right-associative fold.

foldl : {A : Type}{B : Type}(BAB)BList ABSource#

Left-associative and tail-recursive fold.

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

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

filter : {A : Type}(ABool)List AList ASource#

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

length : {A : Type}List ANatSource#

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

reverse : {A : Type}List AList ASource#

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

replicate : {A : Type}NatAList ASource#

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

take : {A : Type}NatList AList ASource#

Takes the first n elements of a List.

drop : {A : Type}NatList AList ASource#

Drops the first n elements of a List.

splitAt : {A : Type}NatList AList 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.

merge : {A : Type}Ord AList AList AList ASource#

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

partition : {A : Type}(ABool)List AList 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 AList AList ASource#

Concatenates two Lists.

snoc : {A : Type} -> List A -> A -> List ASource#

𝒪(𝓃). Append an element.

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

Concatenates a List of Lists.

prependToAll : {A : Type}AList AList ASource#

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

intersperse : {A : Type}AList AList ASource#

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

tail : {A : Type}List AList ASource#

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

any : {A : Type}(ABool)List ABoolSource#

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

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

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

null : {A : Type}List ABoolSource#

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

zipWith : {A : Type} -> {B : Type} -> {C : Type} -> (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 : Type} -> {B : Type} -> List A -> List B -> List (A × B)Source#

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

mergeSort : {A : Type}Ord AList AList ASource#

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

terminating quickSort : {A : Type}Ord AList AList ASource#

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

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

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

concatMap : {A B : Type} -> (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.