[Why3-club] lemma visibility

Claude Marché Claude.Marche at inria.fr
Tue Jan 8 13:44:53 CET 2019


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

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
> 
-------------- next part --------------

module M

  use int.Int
  
  lemma L: 2+2=5

  goal g: false

  meta remove_prop lemma L

end

module N

  use M

  goal g: false

end


More information about the Why3-club mailing list