Specification of an array combinator.
Specification of an array combinator. The indexes of argument and
result sorts refer to the ExtArray
theories
specified as part of the CombArray
theory. The field
definition
of an n
-ary combinator
defines the operation as a relation on the array objects; the
defining formula can contain free variables _0, _1, ...,
_n
, representing the n-1
arguments objects
and the result object, respectively.
(Since version ) see corresponding Javadoc for more information.