[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

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-



More information about the Why3-club mailing list