[Why3-club] lemma visibility

Julia Lawall julia.lawall at lip6.fr
Fri Jan 4 16:48:42 CET 2019


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


More information about the Why3-club mailing list