Documentation

Mathlib.Logic.Function.FromTypes

Function types of a given heterogeneous arity #

This provides Function.FromTypes, such that FromTypes ![α, β] τ = α → β → τ. Note that it is often preferable to use ((i : Fin n) → p i) → τ in place of FromTypes p τ.

Main definitions #

def Function.FromTypes {n : } :
(Fin nType u)Type u → Type u

The type of n-ary functions p 0 → p 1 → ... → p (n - 1) → τ.

Equations
theorem Function.fromTypes_zero (p : Fin 0Type u) (τ : Type u) :
FromTypes p τ = τ
theorem Function.fromTypes_succ {n : } (p : Fin (n + 1)Type u) (τ : Type u) :
theorem Function.fromTypes_cons {n : } (α : Type u) (p : Fin nType u) (τ : Type u) :
FromTypes (Matrix.vecCons α p) τ = (αFromTypes p τ)
def Function.fromTypes_zero_equiv (p : Fin 0Type u) (τ : Type u) :
FromTypes p τ τ

The definitional equality between 0-ary heterogeneous functions into τ and τ.

Equations
@[simp]
theorem Function.fromTypes_zero_equiv_symm_apply (p : Fin 0Type u) (τ : Type u) (a : FromTypes p τ) :
@[simp]
theorem Function.fromTypes_zero_equiv_apply (p : Fin 0Type u) (τ : Type u) (a : FromTypes p τ) :

The definitional equality between ![]-ary heterogeneous functions into τ and τ.

Equations
def Function.fromTypes_succ_equiv {n : } (p : Fin (n + 1)Type u) (τ : Type u) :

The definitional equality between p-ary heterogeneous functions into τ and function from vecHead p to (vecTail p)-ary heterogeneous functions into τ.

Equations
@[simp]
theorem Function.fromTypes_succ_equiv_apply {n : } (p : Fin (n + 1)Type u) (τ : Type u) (a : FromTypes p τ) :
@[simp]
theorem Function.fromTypes_succ_equiv_symm_apply {n : } (p : Fin (n + 1)Type u) (τ : Type u) (a : FromTypes p τ) :
def Function.fromTypes_cons_equiv {n : } (α : Type u) (p : Fin nType u) (τ : Type u) :
FromTypes (Matrix.vecCons α p) τ (αFromTypes p τ)

The definitional equality between (vecCons α p)-ary heterogeneous functions into τ and function from α to p-ary heterogeneous functions into τ.

Equations
@[simp]
theorem Function.fromTypes_cons_equiv_apply {n : } (α : Type u) (p : Fin nType u) (τ : Type u) (a : FromTypes (Matrix.vecCons α p) τ) :
(fromTypes_cons_equiv α p τ) a = a
@[simp]
theorem Function.fromTypes_cons_equiv_symm_apply {n : } (α : Type u) (p : Fin nType u) (τ : Type u) (a : FromTypes (Matrix.vecCons α p) τ) :
def Function.FromTypes.const {n : } (p : Fin nType u) {τ : Type u} (t : τ) :

Constant n-ary function with value t.

Equations
@[simp]
theorem Function.FromTypes.const_zero (p : Fin 0Type u) {τ : Type u} (t : τ) :
const p t = t
@[simp]
theorem Function.FromTypes.const_succ {n : } (p : Fin (n + 1)Type u) {τ : Type u} (t : τ) :
const p t = fun (x : Matrix.vecHead p) => const (Matrix.vecTail p) t
theorem Function.FromTypes.const_succ_apply {n : } (p : Fin (n + 1)Type u) {τ : Type u} (t : τ) (x : p 0) :