Functions that could be used as let-functions
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
oflet function f … = e
is not available to provers - when writing
function f … = e
there is no preconditions tof
, hencef x = e
always holds - pure logic function
f
must be structurally recursive solet 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.