[Why3-club] constant in code

Andrei Paskevich andrei.paskevich at lri.fr
Mon Mar 25 17:55:44 CET 2019


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>
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
> 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/20190325/724fb4a5/attachment.html>


More information about the Why3-club mailing list