Float32

Float32 viewer widget (executable IEEE-754 backend).

Commands:

• #float32_view x renders an IEEE32Exec value as bits + fields + basic classification flags.
• #float32_round_view x shows how a Lean Float (binary64) rounds to IEEE32Exec (binary32).

These widgets are meant for debugging/teaching, not for proof scripts.

Main definitions

• float32Html: inspect class/fields/bits for one IEEE32Exec value.
• float32RoundHtml: show Float64 -> Float32 rounding behavior.
• float32CompareHtml: side-by-side bit-level comparison.
• #float32_view, #float32_round_view, #float32_compare_view: command entry points.

Implementation notes

• Explicit sign/exp/frac bit pills are easier to read than one long bit string when debugging rounding and special values.
• We include both classification badges and raw field values: in practice users want both the high-level class and exact bit-level evidence.
• We keep this widget purely informational; no arithmetic semantics are changed here.

References

• IEEE 754 floating-point standard overview
• ProofWidgets
• Lean community documentation style

Tags

float32, ieee754, rounding, bits, proofwidgets

def NN.Widgets.Float32Internal.u32Hex (u : UInt32) : String

def NN.Widgets.Float32Internal.u64Hex (u : UInt64) : String

def NN.Widgets.Float32Internal.bitsFixed (width n : ℕ) : String

Render exactly width low-order bits of n as a binary string.

def NN.Widgets.Float32Internal.bitPill (label bits bg : String) : ProofWidgets.Html

def NN.Widgets.Float32Internal.classify (x : TorchLean.Floats.IEEE754.IEEE32Exec) : String

Classify an IEEE32 value into normal/subnormal/zero/inf/nan variants.

def NN.Widgets.Float32Internal.dyadicString (d : TorchLean.Floats.IEEE754.IEEE32Exec.Dyadic) : String

def NN.Widgets.float32Html (x : TorchLean.Floats.IEEE754.IEEE32Exec) : ProofWidgets.Html

Render an executable float32 (IEEE32Exec) as HTML.

@[implicit_reducible]

instance NN.Widgets.instTensorElemViewIEEE32Exec : TensorElemView TorchLean.Floats.IEEE754.IEEE32Exec

Element renderer for IEEE32Exec used by #tensor_view.

Renders the float value, with a tooltip that includes a small classification and the raw bit pattern.

def NN.Widgets.Float32Internal.float32CompareHtml (x y : TorchLean.Floats.IEEE754.IEEE32Exec) : ProofWidgets.Html

Compare two IEEE32Exec values at the bit level and render the results as HTML.

def NN.Widgets.Float32Internal.float32RoundHtml (x : Float) : ProofWidgets.Html

Show how a Lean Float (binary64) rounds to an executable float32 (IEEE32Exec, binary32).

Commands

def NN.Widgets.float32ViewCmd : Lean.ParserDescr

def NN.Widgets.«command#float32_view_» : Lean.ParserDescr

def NN.Widgets.float32RoundViewCmd : Lean.ParserDescr

def NN.Widgets.«command#float32_round_view_» : Lean.ParserDescr

def NN.Widgets.float32CompareViewCmd : Lean.ParserDescr

def NN.Widgets.«command#float32_compare_view_,_» : Lean.ParserDescr