Inspection profiles for binary-interchange formats #

Representation, exceptional values, rounding rules, and theorem groups used by #float_info. Info.Command resolves the carrier and supplies its storage and execution details. Complex and interval profiles also use inspectSummary to read their component descriptor.

Each theorem group states its scope. IEEE-specific theorems are marked unavailable when the descriptor does not meet their encoding and bias requirements.

source

structure FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.Summary :

Type

Closed descriptor data extracted by the #float_info elaborator.

expWidth : ℕ
Number of stored exponent bits.
fracWidth : ℕ
Number of stored fraction bits.
exponentBias : ℕ
Bias subtracted from a stored normal exponent.
encoding : FloatFormat.Encoding
Exceptional-value encoding policy.
bitWidth : ℕ
Total encoded width, including the sign bit.
minNormalExponent : ℤ
Smallest unbiased exponent of a normal value.
maxNormalExponent : ℤ
Largest unbiased exponent of a finite normal value.
isIEEE : Bool
Whether the descriptor uses the conventional IEEE bias and exceptional-value encoding.

Instances For

source

def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.inspectSummary (format : Lean.Expr) :

Lean.MetaM Summary

Read the descriptor fields used by scalar, complex, and interval reports.

Instances For

source

def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.encodingName :

FloatFormat.Encoding → String

Human-readable name of a binary exceptional-value policy.

Instances For

source

def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.standardName (summary : Summary) :

String

Identify named IEEE layouts; arbitrary widths retain the more general IEEE-style label.

Instances For

source

def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.nanDescription (encoding : FloatFormat.Encoding) :

String

Precise NaN population and metadata retained by an encoding policy.

Instances For

source

def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.signalingNaNDescription (encoding : FloatFormat.Encoding) (fracWidth : ℕ) :

String

Whether the encoding has a signaling NaN. IEEE signaling NaNs require a nonzero fraction with a clear quiet bit, so at least one fraction bit must lie below the quiet bit.

Instances For

source