[Why3-club] lemma visibility
Jean-Christophe.Filliatre at lri.fr
Tue Jan 8 13:40:52 CET 2019
There is at least one way to do this, which is the following declaration:
meta remove_prop axiom your_lemma
You can insert it either in the module containing the lemma, once you do
not need it anymore, or in a separate module which includes (uses) the
Another possibility is to use several modules and the "clone"
instruction, as follows:
axiom FinalThm: forall x....
lemma LocalLemma1: ...
lemma LocalLemma2: ...
clone export Intf
Here the client module does not see the local lemmas used to prove the
theorem. The "clone export" instruction will (by default) turn the
cloned axiom into a lemma.
Jean-Christophe (and Andrei)
On 1/4/19 4:48 PM, Julia Lawall wrote:
> 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.
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club