# Documentation

Mathlib.Data.List.Func

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

def List.Func.neg {α : Type u} [Neg α] (as : List α) :
List α

Elementwise negation of a list

Instances For
def List.Func.set {α : Type u} [] (a : α) :
List αList α

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

Equations
Instances For

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

Instances For
def List.Func.get {α : Type u} [] :
List αα

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

Equations
Instances For
def List.Func.Equiv {α : Type u} [] (as1 : List α) (as2 : List α) :

Pointwise equality of lists. If lists are different lengths, compare with the default element.

Instances For
def List.Func.pointwise {α : Type u} {β : Type v} {γ : Type w} [] [] (f : αβγ) :
List αList βList γ

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

Equations
Instances For
List αList αList α

Pointwise addition on lists. If lists are different lengths, use zero.

Instances For
def List.Func.sub {α : Type u} [Zero α] [Sub α] :
List αList αList α

Pointwise subtraction on lists. If lists are different lengths, use zero.

Instances For
theorem List.Func.length_set {α : Type u} {a : α} [] {m : } {as : List α} :
List.length (List.Func.set a as m) = max () (m + 1)
theorem List.Func.get_nil {α : Type u} [] {k : } :
= default
theorem List.Func.get_eq_default_of_le {α : Type u} [] (k : ) {as : List α} :
k = default
@[simp]
theorem List.Func.get_set {α : Type u} [] {a : α} {k : } {as : List α} :
theorem List.Func.eq_get_of_mem {α : Type u} [] {a : α} {as : List α} :
a asn, a =
theorem List.Func.mem_get_of_le {α : Type u} [] {n : } {as : List α} :
n < as
theorem List.Func.mem_get_of_ne_zero {α : Type u} [] {n : } {as : List α} :
default as
theorem List.Func.get_set_eq_of_ne {α : Type u} [] {a : α} {as : List α} (k : ) (m : ) :
m kList.Func.get m (List.Func.set a as k) =
theorem List.Func.get_map {α : Type u} {β : Type v} [] [] {f : αβ} {n : } {as : List α} :
n < List.Func.get n (List.map f as) = f ()
theorem List.Func.get_map' {α : Type u} {β : Type v} [] [] {f : αβ} {n : } {as : List α} :
f default = defaultList.Func.get n (List.map f as) = f ()
theorem List.Func.forall_val_of_forall_mem {α : Type u} [] {as : List α} {p : αProp} :
p default((x : α) → x asp x) → (n : ) → p ()
theorem List.Func.equiv_refl {α : Type u} {as : List α} [] :
theorem List.Func.equiv_symm {α : Type u} {as1 : List α} {as2 : List α} [] :
List.Func.Equiv as1 as2List.Func.Equiv as2 as1
theorem List.Func.equiv_trans {α : Type u} {as1 : List α} {as2 : List α} {as3 : List α} [] :
List.Func.Equiv as1 as2List.Func.Equiv as2 as3List.Func.Equiv as1 as3
theorem List.Func.equiv_of_eq {α : Type u} {as1 : List α} {as2 : List α} [] :
as1 = as2List.Func.Equiv as1 as2
theorem List.Func.eq_of_equiv {α : Type u} [] {as1 : List α} {as2 : List α} :
List.length as1 = List.length as2List.Func.Equiv as1 as2as1 = as2
@[simp]
theorem List.Func.get_neg {α : Type u} [] {k : } {as : List α} :
= -
@[simp]
theorem List.Func.length_neg {α : Type u} [Neg α] (as : List α) :
=
theorem List.Func.nil_pointwise {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβγ} (bs : List β) :
List.Func.pointwise f [] bs = List.map (f default) bs
theorem List.Func.pointwise_nil {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβγ} (as : List α) :
List.Func.pointwise f as [] = List.map (fun a => f a default) as
theorem List.Func.get_pointwise {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβγ} (h1 : f default default = default) (k : ) (as : List α) (bs : List β) :
List.Func.get k (List.Func.pointwise f as bs) = f () ()
theorem List.Func.length_pointwise {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβγ} {as : List α} {bs : List β} :
@[simp]
theorem List.Func.get_add {α : Type u} [] {k : } {xs : List α} {ys : List α} :
@[simp]
theorem List.Func.length_add {α : Type u} [Zero α] [Add α] {xs : List α} {ys : List α} :
@[simp]
theorem List.Func.nil_add {α : Type u} [] (as : List α) :
@[simp]
theorem List.Func.add_nil {α : Type u} [] (as : List α) :