# Re: [tlaplus] When to prefer function or operator?

Thanks for getting back to me.

So in my example, from a direct specification perspective, it doesn't matter much; does it affect anything in regards to TLC or TLAPS? Does using an operator perform better during model checking?

On Friday, August 21, 2020 at 10:41:26 AM UTC-4 Stephan Merz wrote:
Section 6.4 of Specifying Systems has a thorough discussion of the tradeoffs between functions and operators [1]. The conclusion is as follows:

When defining an object V, you may have to decide whether to make V an operator that takes an argument or a function. The differences between operators and functions will often determine the decision. [...] If these differences don’t determine whether to use an operator or a function, then the choice is a matter of taste. I usually prefer operators.

Regards,
Stephan

[1] Since the publication of Specifying Systems, recursive operator definitions have been added to TLA+ and therefore the arguments about recursive definitions no longer apply.

On 21 Aug 2020, at 16:34, thomas...@gmail.com <thomas...@xxxxxxxxx> wrote:

There are cases when either a function or operator will solve a task more-or-less equivalently.

For example, both this function and operator accomplish a roughly-equivalent result:

addOne[x \in Nat] == x + 1