**Go backward to** 2.1.2.1 Operation Declarations

**Go up to** 2.1.2 Operations

#### 2.1.2.2 Operation Definitions

OP-DEFN ::= op-defn OP-NAME OP-HEAD TERM
OP-HEAD ::= TOTAL-OP-HEAD | PARTIAL-OP-HEAD
TOTAL-OP-HEAD ::= total-op-head ARG-DECL* SORT
PARTIAL-OP-HEAD ::= partial-op-head ARG-DECL* SORT
ARG-DECL ::= arg-decl VAR+ SORT
VAR ::= SIMPLE-ID

A definition `OP-DEFN` of a total operation with some arguments is
written:

*f* (*V*_{11}, ...,
*V*_{1m1}:*s*_{1}; ...;
*V*_{n1}, ...,
*V*_{nmn}:*s*_{n}):*s* = *T*

When the list of arguments is empty, the definition is simply written:
*f* :*s* = *T*

A definition `OP-DEFN` of a partial operation with some arguments is
written:

*f* (*V*_{11}, ...,
*V*_{1m1}:*s*_{1}; ...;
*V*_{n1}, ...,
*V*_{nmn}:*s*_{n}):? *s* = *T*

When the list of arguments is empty, the definition is simply written:
*f* :? *s* = *T*

It declares the operation name *f* as a total, respectively
partial operation, with a profile having argument sorts *s*_{1}
(*m*_{1} times), ..., *s*_{n} (*m*_{n} times) and
result sort *s*. It also asserts the strong equation:

*f*(*V*_{11}, ..., *V*_{nmn}) = *T*

universally quantified over the declared argument variables
**[CHANGED:]** (which must be distinct, and are the only ones allowed in *T*),
**[]** or just
`*f* = *T*' when the list of arguments is empty.
In each of the above cases, the operation name *f* may occur in
the term *T*, and may have *any* interpretation satisfying
the equation--not necessarily the least fixed point.

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk