# Operators

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```

## Operator attributes

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+`.