# Documentation

Mathlib.Logic.Function.OfArity

# Function types of a given arity #

This provides FunctionOfArity, such that OfArity α β 2 = α → α → β. Note that it is often preferrable 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.
def Function.OfArity (α : Type u) (β : Type u) :
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
Instances For
@[simp]
theorem Function.ofArity_zero (α : Type u) (β : Type u) :
= β
@[simp]
theorem Function.ofArity_succ (α : Type u) (β : Type u) (n : ) :
Function.OfArity α β () = (α)
def Function.OfArity.const (α : Type u) {β : Type u} (b : β) (n : ) :

Constant n-ary function with value a.

Equations
• = b
• = fun (x : α) =>
Instances For
@[simp]
theorem Function.OfArity.const_zero (α : Type u) {β : Type u} (b : β) :
= b
@[simp]
theorem Function.OfArity.const_succ (α : Type u) {β : Type u} (b : β) (n : ) :
= fun (x : α) =>
theorem Function.OfArity.const_succ_apply (α : Type u) {β : Type u} (b : β) (n : ) (x : α) :
=
instance Function.OfArity.OfArity.inhabited {α : Type u_1} {β : Type u_1} {n : } [] :
Equations