[Why3-club] constant in code

Jean-Jacques Levy jean-jacques.levy at inria.fr
Mon Mar 25 19:15:22 CET 2019


Dear Andrei,

many thanks for your quick answer. I finally succeeded in modifying my files to release 1.2.0 … BUT I now have:

- many xxx.contents in my text to translate an xxx Appset into a xxx Set :-(
- to define a virtual ‘selements’ function to have a code version of the ‘elements’ function of the library :-(
_ qualifying the Appmap and Appset modules to avoid clashes with the .contents qualifier, the choose, remove functions on sets

There must be ways for simplifications, but I have to understand what are the actual meanings of:

- use
- clone
- clone import

Is ‘export' still used ? 

Best to all, -JJ-


> Le 25 mars 2019 à 17:55, Andrei Paskevich <andrei.paskevich at lri.fr> a écrit :
> 
> Dear Jean-Jacques,
> 
> "val constant nn : int" should do the trick.
> 
> Best,
> Andrei
> 
> On Mon, 25 Mar 2019 at 17:54, Jean-Jacques Levy <jean-jacques.levy at inria.fr <mailto:jean-jacques.levy at inria.fr>> wrote:
> Dear Why3 Friends, in release 1.2.0, I cannot have global constants in code.
> --------------------------------
> module Test0
> 
> constant nn: int
> 
> let main() = nn
> 
> end
> --------------------------------
> File "bb.mlw", line 5, characters 13-15:
> Logical symbol nn is used in a non-ghost context
> --------------------------------
> how to get around it ?
> 
> Thanks -JJ-
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr <mailto:Why3-club at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club <https://lists.gforge.inria.fr/mailman/listinfo/why3-club>

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20190325/44ae4637/attachment.html>


More information about the Why3-club mailing list