Inspection of Lean's native runtime floats #
#float_info reports native storage, arithmetic, and conversions for Lean's Float32 and
binary64 Float. It lists the Lean 4.34 logical-model bridges with their input conditions and
the certified software refinements for their configured counterparts. Execution of native
arithmetic, including explicit calls through Configured.NativeFPU.Unchecked, also depends on
Lean's compiler, runtime, and host hardware.
def
FloatLib.Floats.Formats.IEEE754.Native.FloatInfo.profile
(bits exponentBits fractionBits : ℕ)
(name storage : String)
:
Storage, operations, and conversion theorems for a Lean native float type.