HomeIsabelle/Phabricator

Remove explicit rounding mode from DoubleToFloat built-in and use the current…

Description

Remove explicit rounding mode from DoubleToFloat built-in and use the current rounding mode, setting it where
necessary. This avoids the need to set a rounding mode on the ARM.

Details

Provenance
dcjmAuthored on Mar 3 2021, 9:55 AM
Parents
rPOLYMLe599babc2102: Implement floating point operations: add, subtract, multiply and divide for…
Branches
Unknown
Tags
Unknown