## 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`

.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information