TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Codebook.Core.Proof

Proof-indexed views of exact finite codebooks #

The views in this module attach erased denotation proofs to the same exact-width runtime bit vector. They introduce no additional executable representation.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.Codebook.At {width : ℕ} {α : Type u} (book : Codebook width α) (value : Numerics.NumericalValue α) :
Type

A codebook word bundled with an erased proof of its complete denotation.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.Codebook.AtFinite {width : ℕ} {α : Type u} (book : Codebook width α) (value : α) :
    Type

    A codebook word bundled with an erased proof of its finite denotation.

    Instances For
      source
      theorem FloatLib.Floats.Formats.Codebook.numericalSystem_denote {width : ℕ} {α : Type u} (book : Codebook width α) (code : book.Code) :
      book.numericalSystem.denote code = book.denote code

      The numerical-system wrapper preserves the codebook's denotation definitionally.