В последней версии Why3 (1.0.0), когда я пытаюсь сделать что-то вроде следующего:
let add_one (n: int) : int = n+1
predicate is_successor_of (n: int) (m: int) = m = add_one n
Я получаю ошибку вида: Файл "../something.why", строка x, символы y-z: несвязанный символ "add_one". Я делаю что-то неправильно? Большинство примеров кода WhyML, которые я видел, на самом деле используют только встроенные/стандартные библиотечные функции, но вызывают другие предикаты, определенные в том же файле. Нет ли аналогичного способа вызова функций, которые я определил в том же файле при определении предиката?
