On Sun, 22 Mar 2020, Andrei Paskevich wrote: > Hi Julia, > > when you call a let-lemma in your code, it behaves in exactly the same way > as a normal function call: you must supply the parameters and prove the > instantiated preconditions. These preconditions do not stay in the context > for the subsequent proof obligations and, normally, there should be no need > to purify the parameters to call the let-lemma. > > Could you please share an example that shows your issue?
I don't think I could make it into anything that is digestible. My assumption was that since there is the row of [precondition]s in the list of proof obligations, that that information was remaining available for subsequent proofs. But if it is notm then no problem. The problem is probably just that since things are different somehow than before when I added the uses of the let lemmas, the subsequent proofs come out in a different way. thanks, julia _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
