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 "../something.why", line x, characters yz: unbound symbol 'add_one'. 私は何か間違ったことをしていますか？私が見た WhyML コードのほとんどの例は、実際には組み込み/標準ライブラリ関数のみを使用していますが、同じファイルで定義された他の述語を呼び出しています。述語を定義するときに、同じファイルで定義した関数を呼び出す同様の方法はありませんか?