TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Codebook.Configured.Core

Configured codebook identity #

A complete lookup denotation determines a codebook family on the common ExecFloat carrier. The selected codebook remains in the type, so equal-width lookup tables are never interchangeable.

source
inductive FloatLib.Floats.ExecFloat.Codebook.Family {width : ℕ} {α : Type u} (book : Formats.Codebook width α) :
Type

Type-level identity retaining a complete lookup denotation.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.Codebook.instEncodedFormatFamily {width : ℕ} {α : Type u} (book : Formats.Codebook width α) :
    Numerics.EncodedFormat (Family book)
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.Codebook.instFormatSemanticsFamily {width : ℕ} {α : Type u} (book : Formats.Codebook width α) :
    Numerics.FormatSemantics (Family book)
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.ExecFloat.Codebook {width : ℕ} {α : Type u} (book : Formats.Codebook width α) :
    Type

    Exact-width executable lookup encoding selected by its complete denotation table.

    Instances For