diff options
| author | Pierre Roux | 2018-08-28 18:56:07 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:35 +0100 |
| commit | d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch) | |
| tree | 9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /kernel/retroknowledge.mli | |
| parent | 79605dabb10e889ae998bf72c8483f095277e693 (diff) | |
Implement classify on primitive float
Diffstat (limited to 'kernel/retroknowledge.mli')
| -rw-r--r-- | kernel/retroknowledge.mli | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 7aaf14e176..2df8a00465 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -21,7 +21,14 @@ type retroknowledge = { retro_f_cmp : (constructor * constructor * constructor * constructor) option; (* FEq, FLt, FGt, FNotComparable *) - retro_refl : constructor option; + retro_f_class : (constructor * constructor * constructor * constructor + * constructor * constructor * constructor * constructor + * constructor) + option; + (* PNormal, NNormal, PSubn, NSubn, + PZero, NZero, PInf, NInf, + NaN *) + retro_refl : constructor option } val empty : retroknowledge |