[Why3-club] Difference between let and function?

David MENTRE dmentre at linux-france.org
Thu Aug 25 18:17:15 CEST 2016


How would you define the difference in WhyML between a "let" and a

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?

Best regards,

More information about the Why3-club mailing list