[Why3-club] Difference between let and function?

Yannick Moy moy at adacore.com
Thu Aug 25 18:23:04 CEST 2016

-- David MENTRE (2016-08-25)
> 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?

AFAIK, yes.
Yannick Moy, Senior Software Engineer, AdaCore

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20160825/f2c2bde5/attachment.html>

More information about the Why3-club mailing list