TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Bounded.Configured.Core

Configured bounded fixed-point identity #

The encoded bounded fixed-point family supplies the public ExecFloat.BoundedFixedPoint type. Its runtime carrier is exactly FixedInt width; overflow policy belongs to explicitly named operations.

source
inductive FloatLib.Floats.ExecFloat.BoundedFixedPoint.Family (radix : Numerics.Radix) (fractionalDigits width : ℕ) :
Type

Type-level identity of a bounded fixed-point grid.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.instEncodedFormatFamily (radix : Numerics.Radix) (fractionalDigits width : ℕ) :
    Numerics.EncodedFormat (Family radix fractionalDigits width)
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.instFormatSemanticsFamily (radix : Numerics.Radix) (fractionalDigits width : ℕ) :
    Numerics.FormatSemantics (Family radix fractionalDigits width)
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.ExecFloat.BoundedFixedPoint (radix : Numerics.Radix) (fractionalDigits width : ℕ) :
    Type

    Fixed-width radix-parametric fixed point with explicit overflow-policy operations.

    Instances For