## Functions that could be used as let-functions

**Disclaimer** this report is *wrong* : a let-function without a contract actually exposes its definition to callers.

**Original Report** (wrong)

A frequent pattern we face when writing why3 code for extraction, is a pure logical function that *only makes use of extractible expressions*. We then have to write the following code, with full duplication of core function definition:

```
function f x… : r = e
let rec function f x… : r ensures { result = e } = e
```

For large definition `e`

with pattern matching or mutual-recursion, this is annoying !
This is the dual situation of a `let function f … = e`

, where `f`

can be used in both code & logic except that (among others):

- the definition
`e`

of`let function f … = e`

is*not*available to provers - when writing
`function f … = e`

there is*no*preconditions to`f`

, hence`f x = e`

always holds - pure logic function
`f`

must be structurally recursive so`let function f`

needs no variant

**Proposal:**

Add a keyword to `function`

definitions in order to have the associated `let rec function ...`

for free.
Alternatively, detect that function definition only contains extractible terms and allow to use it like a `let function`

in code.