在Why3的谓词中调用我自己的函数

Question

使用最新版本的Why3 (1.0.0)，当我尝试执行以下操作时：

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

我得到一个错误的形式: File“../omething.ly”，行x，字符y-z:未绑定的符号'add_one‘。我做错了什么吗？我见过的大多数WhyML代码示例实际上只使用内置/标准库函数，但确实调用了同一文件中定义的其他谓词。在定义谓词时，是否没有类似的方法来调用我在同一文件中定义的函数？

Answer 1

使用function关键字将原始add_one函数定义标记为pure似乎可以做到这一点。这是有道理的，因为副作用不应该在谓词中被接受。