List

List package contains inductive data type definition representing finite parametrized homogenous lists, its generic functions, theorems and examples of usage.

data list (A: U) = nil | cons (a: A) (as: list A)

nil

nil construction is terminal element of list data type.

> let a: list nat = nil in a
EVAL: nil

cons

cons is basic list constructor.

> let a: list nat = cons zero nil in a
EVAL: cons zero nil

Generics

length (A: U): list A → nat

Returns length of a list.

> length nat nil
EVAL: zero

head (A: U): list A → maybe A

Returns just a first element of a list, if any. If none returns nothing.

> head nat nil
EVAL: nothing

tail (A: U): list A → maybe (list A)

Returns just a second field of head cons, if any. If none returns nothing.

> let a:maybe (list nat) = tail nat (cons n1 (cons n2 nil)) in a
EVAL: just (cons (suc (suc zero)) nil)

append (A: U): list A → list A → list A

Concatenates two lists into a new list.

> let a: list nat = append nat nil nil in a
EVAL: nil

reverse (A: U): list A → list A

Reverse a list.

data S = O | P | C opc: list S = cons O (cons P (cons C nil))
> reverse S opc
EVAL: cons C (cons P (cons O nil))

map (A B: U) (f: A → B) : list A → list B

Maps each element of a list to a new list.

> let a: list nat = map nat nat (\(x: nat) -> pred x) (cons n3 nil) in a
EVAL: cons (suc (suc zero)) nil

filter (A: U) (p: A → bool) : list A → list A

Filters a list with a predicate function.

f: nat -> bool = split zero -> true suc -> false
> filter nat f (cons zero (cons n1 (cons n2 (cons n3 (cons zero nil)))))
EVAL: cons zero (cons zero nil)

uncons (A: U): list A -> maybe ((a: A) * (list A))

Splits a list onto a head and a tail and returns a sigma pair.

> uncons nat (cons one (cons zero nil))
EVAL: just ((suc zero,cons zero nil))

foldl (A B: U) (f: B → A → B) (Z: B): list A → B

Folds a list by accumulating a value from the left.

> let a: nat = foldl nat nat (\(x: nat) (y: nat) -> add x y) one (cons zero nil) in a
EVAL: suc zero

foldr (A B: U) (f: A → B → B) (Z: B): list A → B

Folds a list by accumulating a value from the right.

> let b: nat = foldr nat nat (\(x: nat) (y: nat) -> add x y) one (cons zero nil) in b
EVAL: suc zero