Calling my own function in a predicate in Why3

Question

With the latest version of Why3 (1.0.0), when I attempt to do something like the following:

 let add_one (n: int) : int = n+1
 predicate is_successor_of (n: int) (m: int) = m = add_one n

I get an error of the form: File "../something.why", line x, characters y-z: unbound symbol 'add_one'. Am I doing something wrong? Most examples I have seen of WhyML code in fact use only built-in/standard library functions, but do call other predicates defined in the same file. Is there no similar way to call functions I've defined in the same file when defining a predicate?

Answer 1

Marking the original add_one function definition as pure, with the function keyword, seems to do the trick. It makes sense, as side-effects should not be admissible in predicates.