GitLab

TODO: make this a configurable option

+ add 'minInt and 'maxInt attributes for range types
+ add 'eb and 'sb attributes for float types
+ make ieee_float realization compatible with Coq 8.4

* 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.

+ add axioms linking eb, sb, emax and pow2sb and clone them as goal in Float(32/64)
+ modify section dealing with integers
+ update realisation

In a different file, so that we can show the simpler ordering property
first.

Also, I cheat, and add an appropriate lemma to modules/python.mlw.
Maybe this is a good lemma to have in map.Occ, too.