verbalizations with arguments

[kohlhase]

We need a general scheme for verbalizations of functional concepts. Marcel Dreier's B.Sc Thesis has some thoughts on this, which are not quite implemented yet.

But the is more than discussed there. I have been stumbling over the treatment of "$n$-ary" again, which I had marked up as \defi[name=nary]{$n$-ary} or as $n$\defi[name=arity]{ary}. All of this muddles the fact that the word ary is functional and takes $n$ as an argument. Other examples are $\mathal{C}$-derivable and $C^\infty$-manifold or $n$ to $m$ relation.

[Jazzpirate]

#1 contains discussions on that. I think ary should be a unary function with n as argument, e.g.
\symdef[type={\funtype{\NaturalNumbers,\funtype}{\prop}}]{ary}[1]{#1\text{-ary}}

Then #1 proposes to write e.g.:
$f$ is an \ary{$n$}[-ary] function

Come to think of it, \ary is a binary predicate on a positive integer and a function, e.g. \ary{$f$}[ is an ]{$n$}[-ary] function.. Either way, things get tricky, if we want to "type" \ary, since the type would already have to carry the arity...