diff options
| author | Guillaume Bertholon | 2018-07-13 16:22:35 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:03 +0100 |
| commit | b0b3cc67e01b165272588b2d8bc178840ba83945 (patch) | |
| tree | 0fc62f69eb0b56a3cae6dd81f82ca869dac6fbc9 /kernel/cPrimitives.mli | |
| parent | f93684a412f067622a5026c406bc76032c30b6e9 (diff) | |
Add primitive float computation in Coq kernel
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
Diffstat (limited to 'kernel/cPrimitives.mli')
| -rw-r--r-- | kernel/cPrimitives.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3c825a8018..f9424fb09d 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -33,6 +33,18 @@ type t = | Int63lt | Int63le | Int63compare + | Float64opp + | Float64abs + | Float64compare + | Float64add + | Float64sub + | Float64mul + | Float64div + | Float64sqrt + | Float64ofInt63 + | Float64normfr_mantissa + | Float64frshiftexp + | Float64ldshiftexp val equal : t -> t -> bool @@ -55,12 +67,14 @@ val kind : t -> args_red type prim_type = | PT_int63 + | PT_float64 type 'a prim_ind = | PIT_bool : unit prim_ind | PIT_carry : prim_type prim_ind | PIT_pair : (prim_type * prim_type) prim_ind | PIT_cmp : unit prim_ind + | PIT_option : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex |