The conversion of Float
to UInt64
doesn't behave as described in the documentation.
#5483
Closed
3 tasks done
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
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
toUInt64
(etc) doesn't behave as described in the documentation.From
Data/Float.lean
:However, the following seems problematic:
Context
As discussed on Zulip
Steps to Reproduce
Expected behavior:
Actual behavior:
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
The text was updated successfully, but these errors were encountered: