[Why3-club] lemma visibility

Julia Lawall julia.lawall at lip6.fr
Thu Jan 24 12:15:46 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

Is there any way to find out what lemmas alt-ergo is trying to use?  This
could be helpful to figure out what to exclude.

thanks,
julia


More information about the Why3-club mailing list