RFC: Float <-> UInt8/ByteArray conversions

[seanmcl]

Proposal

In order to reason about Python's ndarray type stored on disk, we need to be able to read a file of bytes and interpret it as a Lean Array of Float. Since the float bits are represented in IEEE-754 binary format, we need a way to go from UInt64 or ByteArray to Float and vice versa. There seems to be no way to accomplish this today.

For example, the following code should

#eval
  let f := 1.67
  let n : UInt64 := 0x3FFAB851EB851EB8  -- Closest double to 1.67 in hex
  let f' : Float := Float.ofUInt64Bytes n
  let n' := f.toUInt64Bytes
  f == f' && n == n'

should eval to true.

A brief thread on Zulip where it was deemed impossible to do this today.

[Kha]

RFC accepted! Implementation to follow soon.