[Why3-club] constant in code

Jean-Jacques Levy jean-jacques.levy at inria.fr
Mon Mar 25 17:54:03 CET 2019

Dear Why3 Friends, in release 1.2.0, I cannot have global constants in code.
module Test0

constant nn: int

let main() = nn

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-

More information about the Why3-club mailing list