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

@[instance_reducible]

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

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

Equations

• Encodable.List.Vector.encodable = { encode := Encodable.List.Vector.encodable._aux_1, decode := Encodable.List.Vector.encodable._aux_3, encodek := ⋯ }

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

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

@[instance_reducible]

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

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

Equations

• Encodable.finArrow = Encodable.ofEquiv (List.Vector α n) (Equiv.vectorEquivFin α n).symm

@[instance_reducible]

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

Equations

• Encodable.finPi n π = Encodable.ofEquiv { f : Fin n → (i : Fin n) × π i // ∀ (i : Fin n), (f i).fst = i } (Equiv.piEquivSubtypeSigma (Fin n) π)

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.

Equations

• Encodable.fintypeArrow α β = Trunc.map (fun (f : α ≃ Fin (Fintype.card α)) => Encodable.ofEquiv (Fin (Fintype.card α) → β) (f.arrowCongr (Equiv.refl β))) (Fintype.truncEquivFin α)

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.

Equations

• One or more equations did not get rendered due to their size.

@[instance_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.

Equations

• Encodable.fintypeArrowOfEncodable = Encodable.ofEquiv (Fin (Fintype.card α) → β) (Encodable.fintypeEquivFin.arrowCongr (Equiv.refl β))