TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.OCP.MX.E8M0.Info

Inspection reports for OCP E8M0 and raw MX blocks #

This optional meta module registers #float_info for the raw E8M0 scale and BlockCode types. Executable decoding remains in Core, Semantics, and Block, so runtime-only clients do not depend on command elaboration or report rendering.

Reports distinguish scale decoding from joint block decoding and list their refinement theorems. The raw block type admits arbitrary lengths and element descriptors.

source
def FloatLib.Floats.Formats.OCP.MX.E8M0.FloatInfo.Command.profile :
ExecFloat.FormatProfile

Build the E8M0 inspection profile shared by the raw code and configured ExecFloat wrapper.

Instances For
    source
    def FloatLib.Floats.Formats.OCP.MX.E8M0.FloatInfo.Command.blockElementIdentity (format : Lean.Expr) :
    Lean.MetaM String

    Human-readable identity for a binary element descriptor used in an E8M0-scaled block.

    Instances For
      source
      def FloatLib.Floats.Formats.OCP.MX.E8M0.FloatInfo.Command.blockProfile (elementIdentity : String) :
      ExecFloat.FormatProfile

      Build the report for the joint shared-scale-and-elements block carrier.

      Instances For