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 #

Float32.html: inspect class/fields/bits for one ExecFloat.Binary 8 23 value.
Float32.roundHtml: show Float64 -> Float32 rounding behavior.
Float32.compareHtml: side-by-side bit-level comparison.
#float32_view, #float32_round_view, #float32_compare_view: command entry points.

source

def NN.Widgets.Float32.hex {width : ℕ} (bits : BitVec width) :

String

Render a bit vector in hexadecimal, preserving the width encoded by its type.

Instances For

source

def NN.Widgets.Float32.bitsFixed (width n : ℕ) :

String

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

Instances For

source

def NN.Widgets.Float32.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.

Instances For

source

def NN.Widgets.Float32.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.

Instances For

source

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

String

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

The significand and exponent come from FloatLib's decoded dyadic value; the sign is kept explicit even for zero.

Instances For

source

def NN.Widgets.Float32.html (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) :

ProofWidgets.Html

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

Instances For

source

@[instance_reducible]

instance NN.Widgets.Float32.instTensorElemViewBinaryOfNatNatIeeeDefaultBiasForKnownWidthDescriptorHAddCode :

TensorElemView (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)

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.

source

def NN.Widgets.Float32.compareHtml (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.

Instances For

source

def NN.Widgets.Float32.roundHtml (x : Float) :

ProofWidgets.Html

Show how a Lean Float (binary64) rounds to an executable float32 (ExecFloat.Binary 8 23, binary32).

The result is widened to native binary64 for its decimal display. The displayed difference is computed by native binary64 subtraction; it is not an exact-real error certificate.

Instances For