Float32

Float32 viewer widget (executable IEEE-754 backend).

Commands:

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

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

Main definitions

• float32Html: inspect class/fields/bits for one ExecFloat.Binary 8 23 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.

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

Compact rendering of a 32-bit word for the bit-pattern pills.

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

The 64-bit counterpart, used when a widget shows a binary64 input alongside its float32 result.

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

One labelled, colour-coded run of bits: the sign, exponent and fraction fields each get one.

Colours are given as rgba overlays rather than solid fills so the widget stays readable against both light and dark editor themes.

def NN.Widgets.Float32Internal.classify (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) classify._proof_1 classify._proof_2 classify._proof_3 classify._proof_4) : String

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

def NN.Widgets.Float32Internal.dyadicString (d : FloatLib.Numerics.Dyadic) : String

Render a dyadic rational as ±mantissa * 2^exponent.

This is the exact value of a finite float, written the way Flocq and Coq's Fappli_IEEE write it, so what the widget shows can be compared directly against the proofs.

def NN.Widgets.float32Html (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Float32Internal.classify._proof_1 Float32Internal.classify._proof_2 Float32Internal.classify._proof_3 Float32Internal.classify._proof_4) : ProofWidgets.Html

Render an executable float32 (ExecFloat.Binary 8 23) as HTML.

@[instance_reducible]

instance NN.Widgets.instTensorElemViewBinaryOfNatNatIeeeDefaultBias : TensorElemView (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) Float32Internal.classify._proof_1 Float32Internal.classify._proof_2 Float32Internal.classify._proof_3 Float32Internal.classify._proof_4)

Element renderer for ExecFloat.Binary 8 23 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 : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) classify._proof_1 classify._proof_2 classify._proof_3 classify._proof_4) : ProofWidgets.Html

Compare two ExecFloat.Binary 8 23 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 (ExecFloat.Binary 8 23, 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