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?
Best,
Andrei
On Sun, 22 Mar 2020 at 13:46, Julia Lawall <julia.law...@lip6.fr> wrote:
> Hello,
>
> I have the impression that when using a let lemma as code, one gets asked
> to prove all the preconditions, that then clutter up the space of known
> things, making other things harder to prove. In my case, I have to add a
> lot of let x = pure { y } declarations to be able to use the let lemma. I
> don't know if this is an issue.
>
> Is there a way to write or use a let lemma such that its preconditions
> will somehow be local to the use of the lemma and disappear when proving
> other things?
>
> Or have I completely misunderstood the issue.
>
> thanks,
> 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
