TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Configured.Core

Configured exact fixed-point identity #

The encoded exact fixed-point family supplies the public ExecFloat.FixedPoint type. Executable operations, refinement proofs, planner metadata, and dispatch instances live in downstream modules.

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

Type-level identity of an exact fixed-point grid.

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

    Exact radix-parametric fixed point on the common executable carrier.

    Instances For