RosettaCodeData/Task/Variadic-function/Coq/variadic-function-1.coq

Fixpoint Arity (A B: Set) (n: nat): Set := match n with
|O => B
|S n' => A -> (Arity A B n')
end.