BASIC-ITEM ::= ... | ATTRIBUTION ATTRIBUTION ::= attribution PROPERTY+ FUN-SYMB+ PROPERTY ::= SIMPLE-PROPERTY | UNIT-PROPERTY SIMPLE-PROPERTY ::= associative | commutative | idempotent UNIT-PROPERTY ::= unit-property FUN-SYMB
[AT] Does UNIT-PROPERTY declare FUN-SYMB or must it be declared elsewhere?
Discharged: It must be declared elsewhere; attributions are purely axiomatic.An ATTRIBUTION of some properties to some function symbols FUN-SYMB+ abbreviates evident axioms 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--in particular, this generally requires that each specified function symbol takes two arguments, both of the same sort.
Discharged: These are included.
[TM] I suppose that there is no effect on well-formedness of infix terms. E.g. with and without the declarationthe term x+y+z is either ill-formed or has a parse (either (x+y)+z or x+(y+z)) which is fixed, in advance, once and for all.assoc +
Discharged: This seems reasonable.