Suppose you want to call the lemma on (old x). When the value of x that
you are interested in is current (e.g. at the start of the function),
you can take a snapshot of it using "pure" :
"let ghost ox = pure { x } in ..." You may then call your let lemma on
ox at a later point.
Raphaël
On 03/10/2019 11:30, Julia Lawall wrote:
It seems that I cannot use (old ...) in calling my let lemma? Is there a
way around this?
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
