TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Interval.Info

Proof-aware inspection of executable binary intervals #

The #float_info registration for Model.Interval fmt describes its carrier and proved enclosure contracts. Interval operations are deliberately reported as an outward-rounded specialized API, not as scalar ExecFloat capabilities. The report distinguishes the raw two-endpoint carrier from Interval.Valid, and it names the exact hypotheses under which each operation is a proved real or extended-real enclosure.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.FloatInfo.BinarySummary :
Type

Descriptor summary reused by the interval-format inspection report.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.FloatInfo.profile (summary : BinarySummary) :
    ExecFloat.FormatProfile

    Build the execution and enclosure-proof profile for a binary endpoint interval.

    Instances For