Function symbol not found in a block of mutually recursive definitions
Consider the following example:
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
Why3 complains with an unbound function error for the postcondition of f
. Is this the expected behavior? Since g
is defined using with function
, I supposed it would be bound also for the contract of f
.