TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Storage.Codecs

Storage codecs for configured posits #

Every storage plan uses the same canonical Code conversion pair. The plan remains reducible, so a closed configured posit still specializes to its selected primitive, pair, or wide carrier.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.Posit.Configured.canonicalCodec (format : Format) (plan : StoragePlan format) :
ExecFloat.ModelCodec plan (Model format) (Code plan)

The canonical lossless codec for one statically known storage plan.

Keeping the record construction in one place avoids duplicating conversion code and inverse proofs across the primitive, pair, and wide carriers.

Instances For
    source
    @[reducible, inline]
    instance FloatLib.Floats.Formats.Posit.Configured.codecForPlan (format : Format) (plan : StoragePlan format) :
    ExecFloat.ModelCodec plan (Model format) (Code plan)

    The lossless codec selected by an arbitrary static storage plan.

    The match precedes codec-record construction so native code generation sees the selected unboxed carrier before compiling record projections. Every branch still uses the same generic codec.