An operator is declared with the keyword `op`

:

`op `

*<op-name>*` : `

*<arity>*` -> `

*<sort-of-op>*` { `

*<operator-attribute>*` }`

The name of the operator is written in *<op-name>*. The arity and the the coarity of the operator are written in *<arity>* and *<sort-of-op>* respectively. An arity is a sequence of sorts and a coarity is a single sort. An operator takes a list of elements according to its arity and returns an element of its coarity. A pair of the arity and the coarity is called the rank. Operator attributes will be explained later.

Operators which have exactly the same rank can be declared with `ops`

simultaneously.

`ops `

*<op-name>*` `

...` `

*<op-name>*` : `

*<arity>*` -> `

*<sort-of-op>*` { `

*<operator-attribute>*` }`

In CafeOBJ, places of arguments of operators can be designated by underbars. Operators including underbars are called mix-fix operators. For example, `_+_`

is an infix operator. Mix-fix operators give us a way to declare more flexible argument positions like `while_do_od`

.

Examples:

```
** Constants (The arity is empty)
ops true false : -> Bool
** Infix operator
op _+_ : Nat Nat -> Nat
** Mix-fix operator
op if_then_else_if : Bool Exp Exp -> Exp
** Juxtaposition ('e1 e2 e3 ... en nil' can be a term of Sequence)
op __ : Elt Sequence -> Sequence
```

Operators can be declared with attributes. There are several useful attributes.

`assoc`

: Associativity`comm`

: Commutativity`idem`

: Idempotency`idr:`

*<op-name>*: identity`r-assoc`

: Right-assosiativity (for parsing terms)`l-assoc`

: Left-assosiativity (for parsing terms)`prec:`

*<precedence>*: Precedence (for parsing terms. Larger integer, stronger connectivity)`strat: (`

*<e-strategy>*`)`

: Strategy (for reducing terms)

See CafeOBJ manual for more details.

For example, the associative and commutative operator `+`

in NAT+ can be declared as follows:

mod! NAT+AC { pr(NAT+) op _+_ : Nat Nat -> Nat { assoc comm } }

Module `NAT+AC`

denotes the same model with the module obtained by adding the equations `eq (X + Y) + Z = X + (Y + Z) .`

and `eq X + Y = Y + X .`

to `NAT+`

.

Original Copyright © Takahiro Seino, all rights reserved.