[Why3-club] Difference between let and function?

Andrei Paskevich andrei.paskevich at lri.fr
Fri Aug 26 09:24:26 CEST 2016

On 25 August 2016 at 18:17, David MENTRE <dmentre at linux-france.org> wrote:
> Hello,
> How would you define the difference in WhyML between a "let" and a
> "function"?
> As far as I understood it, "function" is pure logical function, without
> side effect. Its body is visible and can be expanded. On the contrary,
> "let" is an "opaque" function definition only seen through its contract.
> It can have side effects.
> Am I correct?

Yes, this is correct. I would also add that functions are "visible"
and let-functions are "opaque" with respect to provers (and not wrt
exection, for example). Also, logical functions can currently be used
inside let-functions (I try to call them "routines" to distinguish
them from logical functions), but not vice versa.


More information about the Why3-club mailing list