[Why3-club] lemma visibility

Julia Lawall julia.lawall at lip6.fr
Mon Mar 11 07:36:15 CET 2019



On Tue, 8 Jan 2019, Claude Marché wrote:

>
> Hello,
>
> The easiest way to achieve this is to add, at the end of the module that needs
> a lemma "L" only internally, the declaration
>
> See attached file for example
>
> meta remove_prop lemma L

I never got this to work.  Actually my lemma is declared with let rec
lemma.  Why3 says that it is not a proposition.

julia


>
> Hope this helps,
>
> Le 04/01/2019 à 16:48, Julia Lawall a écrit :
> > Is it possible to make a lemma only visible within a module, but not
> > visible to other modules that may import the module?  It seems that the
> > presence or absence of some irrelevant lemmas can have a big impact on
> > whether at least Alt-Ergo can succeed in doing some proofs in a reasonable
> > amount of time.
> >
> > thanks,
> > julia
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
>


More information about the Why3-club mailing list