This provides FunctionOfArity, such that OfArity α β 2 = α → α → β.
Note that it is often preferrable to use (Fin n → α) → β in place of OfArity n α β.
OfArity α β 2 = α → α → β
(Fin n → α) → β
OfArity n α β
Function.OfArity α β n
α → α → ... → β
Function.OfArity.const α b n
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 β.
Unit → β
Constant n-ary function with value a.