diff options
| author | Guillaume Bertholon | 2018-08-03 17:38:48 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:27 +0100 |
| commit | dda50a88aab0fa0cfb74c8973b5a4353fe5c8447 (patch) | |
| tree | ad80b6386f39dda5666308658ef7d9fa79c4cd20 /kernel/cPrimitives.ml | |
| parent | 55d32c9f3a91058f69f34c17c17701d0dc81874d (diff) | |
Put axioms on ldshiftexp and frshiftexp
Axioms on ldexp and frexp are replaced by proofs inside FloatLemmas.
The shift value has been increased to 2 * emax + prec because in ldexp
we want to be able to transform the smallest denormalized to the biggest
float value in one call.
Diffstat (limited to 'kernel/cPrimitives.ml')
0 files changed, 0 insertions, 0 deletions