Function types of a given arity

This provides Function.OfArity, such that OfArity α β 2 = α → α → β. Note that it is often preferable to use (Fin n → α) → β in place of OfArity n α β.

Main definitions

• Function.OfArity α β n: n-ary function α → α → ... → β. Defined inductively.
• Function.OfArity.const α b n: n-ary constant function equal to b.

@[reducible, inline]

abbrev Function.OfArity (α : Type u) (β : Type u) (n : ℕ) : Type u

The type of n-ary functions α → α → ... → β.

Note that this is not universe polymorphic, as this would require that when n=0 we produce either Unit → β or ULift β.

Equations

• Function.OfArity α β n = Function.FromTypes (fun (x : Fin n) => α) β

@[simp]

theorem Function.ofArity_zero (α : Type u) (β : Type u) : Function.OfArity α β 0 = β

@[simp]

theorem Function.ofArity_succ (α : Type u) (β : Type u) (n : ℕ) : Function.OfArity α β n.succ = (α → Function.OfArity α β n)

def Function.OfArity.const (α : Type u) {β : Type u} (b : β) (n : ℕ) : Function.OfArity α β n

Constant n-ary function with value b.

Equations

• Function.OfArity.const α b n = Function.FromTypes.const (fun (x : Fin n) => α) b

@[simp]

theorem Function.OfArity.const_zero (α : Type u) {β : Type u} (b : β) : Function.OfArity.const α b 0 = b

@[simp]

theorem Function.OfArity.const_succ (α : Type u) {β : Type u} (b : β) (n : ℕ) : Function.OfArity.const α b n.succ = fun (x : Matrix.vecHead fun (x : Fin n.succ) => α) => Function.OfArity.const α b n

theorem Function.OfArity.const_succ_apply (α : Type u) {β : Type u} (b : β) (n : ℕ) (x : α) : Function.OfArity.const α b n.succ x = Function.OfArity.const α b n

instance Function.OfArity.inhabited {α : Type u_1} {β : Type u_1} {n : ℕ} [Inhabited β] : Inhabited (Function.OfArity α β n)

Equations

• Function.OfArity.inhabited = inferInstanceAs (Inhabited (Function.FromTypes (fun (x : Fin n) => α) β))

theorem Function.FromTypes.fromTypes_fin_const (α : Type u) (β : Type u) (n : ℕ) : Function.FromTypes (fun (x : Fin n) => α) β = Function.OfArity α β n

def Function.FromTypes.fromTypes_fin_const_equiv (α : Type u) (β : Type u) (n : ℕ) : Function.FromTypes (fun (x : Fin n) => α) β ≃ Function.OfArity α β n

The definitional equality between heterogeneous functions with constant domain and n-ary functions with that domain.

Equations

• Function.FromTypes.fromTypes_fin_const_equiv α β n = Equiv.refl (Function.FromTypes (fun (x : Fin n) => α) β)