Encodability of Pi types

This file provides instances of Encodable for types of vectors and (dependent) functions:

• Encodable.List.Vector.encodable: vectors of length n (represented by lists) are encodable
• Encodable.finArrow: vectors of length n (represented by Fin-indexed functions) are encodable
• Encodable.fintypeArrow, Encodable.fintypePi: (dependent) functions with finite domain and countable codomain are encodable

@[implicit_reducible]

instance Encodable.List.Vector.encodable {α : Type u_1} [Encodable α] {n : ℕ} : Encodable (List.Vector α n)

If α is encodable, then so is Vector α n.

instance Encodable.List.Vector.countable {α : Type u_1} [Countable α] {n : ℕ} : Countable (List.Vector α n)

If α is countable, then so is Vector α n.

@[implicit_reducible]

instance Encodable.finArrow {α : Type u_1} [Encodable α] {n : ℕ} : Encodable (Fin n → α)

If α is encodable, then so is Fin n → α.

@[implicit_reducible]

instance Encodable.finPi (n : ℕ) (π : Fin n → Type u_2) [(i : Fin n) → Encodable (π i)] : Encodable ((i : Fin n) → π i)

def Encodable.fintypeArrow (α : Type u_2) (β : Type u_3) [DecidableEq α] [Fintype α] [Encodable β] : Trunc (Encodable (α → β))

When α is finite and β is encodable, α → β is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

def Encodable.fintypePi (α : Type u_2) (π : α → Type u_3) [DecidableEq α] [Fintype α] [(a : α) → Encodable (π a)] : Trunc (Encodable ((a : α) → π a))

When α is finite and all π a are encodable, Π a, π a is encodable too. Because the encoding is not unique, we wrap it in Trunc to preserve computability.

@[implicit_reducible]

instance Encodable.fintypeArrowOfEncodable {α : Type u_2} {β : Type u_3} [Encodable α] [Fintype α] [Encodable β] : Encodable (α → β)

If α and β are encodable and α is a fintype, then α → β is encodable as well.