fix: don't show NaN sign info in Float.toString

[digama0]

• Depends on: fix: use saturating casts in lean_float_to_uint8 to avoid UB #1458 (it adds a test to the same file)

This is another issue identified in the Zulip thread: Because the NaN sign bit and payload bits are architecture-dependent and not specified by IEEE 754, the simplest way to prevent this from affecting Lean code is to treat Float as a quotient type with respect to the various NaN values. Because the actual type is opaque to lean, it is possible to do this "in our hearts" with no code changes. The only exception to this is Float.toString, which becomes a non-function under this model as it distinguishes equal values.

This is still not really observable without native_decide because the kernel doesn't know how any of these functions compute, but we should still try to keep native_decide sound where possible, so the fix implemented here is to make Float.toString print all NaNs the same, as the string "nan". (Some languages like to write it NaN; bikeshed away.)

[Kha]

I have a slight preference for NaN (same as in Rust)