An ATTRIBUTION of some properties to some function symbols
FUN-SYMB+ determines evident sentences asserting that each of
the functions is to have each of the specified properties. Here, a
FUN-SYMB that is just a FUN-NAME (without an explicit
FUN-TYPE) abbreviates the list of all those function symbols
declared in the local environment whose name has the same identifier
as the specified FUN-NAME. The ATTRIBUTION is
well-formed just when the axioms that it abbreviates are
well-formed--this generally requires that each specified function
symbol is declared (elsewhere) to take two arguments, both of the same
sort, and that the symbol specified in a UNIT-PROPERTY is
declared (elsewhere) as a constant of the appropriate sort.
! ATTRIBUTION ::= attribution PROPERTY+ FUN-SYMB+
! PROPERTY ::= SIMPLE-PROPERTY | UNIT-PROPERTY
! SIMPLE-PROPERTY ::= associative | commutative | idempotent
! UNIT-PROPERTY ::= unit-property FUN-SYMB
CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk