В последней версии 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, символы...