The conversion of Float to UInt64 doesn't behave as described in the documentation.

[TomasPuverle]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The conversion of Float to UInt64 (etc) doesn't behave as described in the documentation.

From Data/Float.lean:

/-- If the given float is positive, truncates the value to the nearest positive integer.
If negative or larger than the maximum value for UInt64, returns 0. -/
@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64

However, the following seems problematic:

def inf : Float := 1.0 / 0.0

-- All of the statements below return true
#eval Float.isInf inf
#eval inf.toUInt64.toNat == (UInt64.size - 1)
#eval (UInt64.size.toFloat * 2).toUInt64.toNat == (UInt64.size - 1)

Context

As discussed on Zulip

Steps to Reproduce

1. See the code above

Expected behavior:

• Either fix the code to return 0
• Update documentation to reflect that the "largest Uint64 value" is returned

Actual behavior:

• Currently returns UIntXX.size - 1

Versions

"4.12.0, commit 5dea30f", MacOS

Additional Information

I'm happy to create a PR, either to fix the behavior or the documentation.

Impact

[Kha]

Yes, the documentation is wrong. Docfix appreciated.

[TomasPuverle]

PR is up: #5497