TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Codebook.Info

Codebook format inspection #

Codebook formats assign a meaning to every stored word by an explicit finite table. Their inspection output therefore reports the table-defined denotation and only the operations whose refinement theorems are actually available; it does not infer arithmetic from bit width.

Catalog entries additionally report their word denotations and finite-input arithmetic theorems. Custom tables receive the generic representation and nearest-codeword guarantees. The public family entry point is FloatLib.Floats.Formats.Codebook.

source
inductive FloatLib.Floats.Formats.Codebook.FloatInfo.CatalogIdentity :
Type

The known catalog identity, when the inspected codebook is one supplied by FloatLib.

Instances For
    source
    def FloatLib.Floats.Formats.Codebook.FloatInfo.catalogIdentity (book : Lean.Expr) :
    CatalogIdentity

    Recognize public catalog entries without guessing from the storage width.

    Instances For
      source
      def FloatLib.Floats.Formats.Codebook.FloatInfo.theoremSurfaces (identity : CatalogIdentity) :
      List ExecFloat.TheoremSurface

      Checked theorem surfaces for the selected codebook.

      Instances For
        source
        def FloatLib.Floats.Formats.Codebook.FloatInfo.rawSpecializedOperations (identity : CatalogIdentity) :
        List ExecFloat.InfoEntry

        Operations implemented by the raw catalog code, without implying universal scalar dispatch.

        Instances For
          source
          def FloatLib.Floats.Formats.Codebook.FloatInfo.configuredSpecializedOperations (identity : CatalogIdentity) :
          List ExecFloat.InfoEntry

          Operations outside universal configured dispatch.

          Bipolar multiplication is omitted here because the configured family installs it as the ordinary proof-linked ExecFloat.Mul capability. Its exact negation remains a family-specific operation. The ternary operations remain checked Option APIs, so both are specialized.

          Instances For
            source
            def FloatLib.Floats.Formats.Codebook.FloatInfo.profile (width : ℕ) (identity : CatalogIdentity) :
            ExecFloat.FormatProfile

            Build the proof-aware profile for an exact-width lookup encoding.

            Instances For