# Lists as Functions #

Definitions for using lists as finite representations of finitely-supported functions with domain ℕ.

These include pointwise operations on lists, as well as get and set operations.

## Notations #

An index notation is introduced in this file for setting a particular element of a list. With `as`

as a list `m`

as an index, and `a`

as a new element, the notation is `as {m ↦ a}`

.

So, for example
`[1, 3, 5] {1 ↦ 9}`

would result in `[1, 9, 5]`

This notation is in the locale `list.func`

.

Update element of a list by index. If the index is out of range, extend the list with default elements

## Equations

- List.Func.set a (head :: as) 0 = a :: as
- List.Func.set a [] 0 = [a]
- List.Func.set a (h :: as) (Nat.succ k) = h :: List.Func.set a as k
- List.Func.set a [] (Nat.succ k) = default :: List.Func.set a [] k

## Instances For

Update element of a list by index. If the index is out of range, extend the list with default elements

## Instances For

Get element of a list by index. If the index is out of range, return the default element

## Equations

- List.Func.get x [] = default
- List.Func.get 0 (a :: tail) = a
- List.Func.get (Nat.succ n) (head :: as) = List.Func.get n as

## Instances For

Pointwise operations on lists. If lists are different lengths, use the default element.

## Equations

- List.Func.pointwise f [] [] = []
- List.Func.pointwise f [] (b :: bs) = List.map (f default) (b :: bs)
- List.Func.pointwise f (a :: as) [] = List.map (fun x => f x default) (a :: as)
- List.Func.pointwise f (a :: as) (b :: bs) = f a b :: List.Func.pointwise f as bs