op

op <op-spec> : <sorts> -> <sort> { <attribute-list> }

Defines an operator by its domain, co-domain, and the term construct. <sorts> is a space separated list of sort names, <sort> is a single sort name. <op-spec> can be of the following forms:

prefix-spec ~ the <op-spec> does not contain a literal _: This defines a normal prefix operator with domain <sorts> and co-domain <sort>

Example: `op f : S T -> U`

mixfix-spec ~ the <op-spec> contains exactly as many literal _ as there are sort names in <sorts>: This defines an arbitrary mixfix (including postfix) operator where the arguments are inserted into the positions designated by the underbars.

Example: `op _+_ : S S -> S`

For the description of <attribute-list> see the entry for operator attributes.