Stdlib.Data.List.Base

Contents

import Juvix.Builtin.V1.List open public

isElement {A} (eq : A -> A -> Bool) (elem : A) : (list : List A) -> BoolSource #

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

find {A} (predicate : A -> Bool) : (list : List A) -> Maybe ASource #

𝒪(𝓃). Returns the leftmost element of the list satisfying the predicate or nothing if there is no such element.

listRfor {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> BSource #

liftFoldr {A B} (fun : A -> B -> B) (acc : B) (list : List A) : BSource #

Right-associative fold.

listFoldl {A B} (fun : B -> A -> B) (acc : B) : (list : List A) -> BSource #

Left-associative and tail-recursive fold.

listFor : {A B : Type} -> (B -> A -> B) -> B -> List A -> BSource #

listMap {A B} (fun : A -> B) : (list : List A) -> List BSource #

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

filter {A} (predicate : A -> Bool) : (list : 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} (list : List A) : NatSource #

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

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

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

replicate {A} : (resultLength : Nat) -> (value : A) -> List ASource #

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

take {A} : (elemsNum : Nat) -> (list : List A) -> List ASource #

Takes the first elemsNum elements of a List.

drop {A} : (elemsNum : Nat) -> (list : List A) -> List ASource #

Drops the first elemsNum elements of a List.

splitAt {A} : (prefixLength : Nat) -> (list : List A) -> Pair (List A) (List A)Source #

𝒪(𝓃). Returns a tuple where first element is the prefix of the given list of length prefixLength and second element is the remainder of the List.

terminating merge {A} {{Ord A}} (list1 list2 : List A) : List ASource #

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

partition {A} (predicate : A → Bool) : (list : List A) -> Pair (List A) (List A)Source #

𝒪(𝓃). 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} -> (list1 : List A) -> (list2 : List A) -> List ASource #

Concatenates two Lists.

snoc {A} (list : List A) (elem : A) : List ASource #

𝒪(𝓃). Append an element.

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

Concatenates a List of Lists.

prependToAll {A} (separator : A) : (list : List A) -> List ASource #

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

intersperse {A} (separator : A) (list : List A) : List ASource #

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

tail {A} (list : List A) : List ASource #

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

head {A} (defaultValue : A) (list : List A) : ASource #

any {A} (predicate : A -> Bool) : (list : List A) -> BoolSource #

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

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

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

isEmpty {A} (list : List A) : BoolSource #

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

zipWith {A B C} (fun : A -> B -> C) : (list1 : List A) -> (list2 : 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} : (list1 : List A) -> (list2 : List B) -> List (Pair A B)Source #

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

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

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

terminating quickSort {A} {{Ord A}} (list : List A) : List ASource #

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

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

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

concatMap {A B} (fun : A -> List B) (list : 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} : (listOfLists : List (List A)) -> List (List A)Source #

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

Description

Definitions