HomeIsabelle/Phabricator

Add a regression test for conversion. This currently fails because Real/32.

Description

Add a regression test for conversion. This currently fails because Real/32.fromString does not recognise "nan", "inf" etc.

Details

Provenance
dcjmAuthored on Nov 8 2023, 8:56 PM
Parents
rPOLYML1c7f93897ff3: Replace Gay code for real number conversion with an ML version of the Ryu…
Branches
Unknown
Tags
Unknown