* declare range types and float types,
* use integer (resp. real) literals for those types through casting,
* specify how to print them in drivers.
Change in syntax
* use
type t = < range 1 2 > (* integers from 1 to 2 *)
type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
the two projections :
t'int
t''real
and the predicate :
t''isFinite
* Restrict the use of "'" in whyml:
Users are not allowed to introduce names where a quote symbol
is followed by a letter. Thus, the following identifiers are
valid:
t'
toto'0''
toto'_phi
whereas toto'phi is not.
Note: we do not yet support negative numbers in range declaration
and casting of a literal.