TicTacToe - 0.1.0

Stdlib.Data.List.Base

Contents

# Definitions

import Juvix.Builtin.V1.List open public

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

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

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

Right-associative fold.

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

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

Left-associative and tail-recursive fold.

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

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

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

{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.

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

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

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

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

Takes the first n elements of a List.

Drops 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.

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

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

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

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

Concatenates two Lists.

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

𝒪(𝓃). Append an element.

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

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.

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

{A} (a : A) : List A -> ASource#

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

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

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

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

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

{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.

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

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

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

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

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

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

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

{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.

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