Hello Marc,
Yes it is an intentional additional feature. As explained briefly by
Francois, a function of profile
let lemma f (x1:t1) .. (x_k:t_k) : t requires {P} ensures {Q}
is turned into the hypothesis
forall x1:t_1,..,x_k:t_k. P -> exists result:t. Q
By the way, I am always interested in recording all the courses taught
using Why3 : is there a web page or any kind of public reference to your
lectures ? Thank you very much in advance !
- Claude
Le 24/06/2019 à 13:40, Marc Schoolderman a écrit :
Dear all,
While teaching a course Why3, my students stumbled upon the fact that a
let lemma can have a return type other than unit.
This was not the case in older versions of Why3 (at least, pre 1.0)
Is this an intentional change/feature?
Best regards,
Marc Schoolderman
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
