[Why3-club] lemma visibility

Raphael Rieu-Helft raphael.rieu-helft at lri.fr
Mon Mar 11 12:03:01 CET 2019


Hello,

For "let lemmas", use `meta remove_prop axiom L`.

Raphaël

On 11/03/2019 07:36, Julia Lawall wrote:
>
> 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
> >
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190311/75170334/attachment.html>


More information about the Why3-club mailing list