# 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) listCase (A C:U) (a b: C): list A -> C listRec (A C:U) (z: C) (s: A->list A->C->C): (n:list A) -> C listElim (A: U) (C:list A->U) (z: C nil) (s: (x:A)(xs:list A)->C(cons x xs)): (n:list A) -> C(n) listInd (A: U) (C:list A->U) (z: C nil) (s: (x:A)(xs:list A)->C(xs)->C(cons x xs)): (n:list A) -> C(n) ```

## 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`