TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Numerics.Core.Declaration

Static format declarations #

float_format declares a format identity, code type, scalar domain, and denotation:

float_format MyFormat where
  Code := UInt8
  Scalar := Rat
  denote := fun bits => ...

The tag has no constructors and occupies no runtime field; values store Code. The generated semantic instance is noncomputable to allow real-valued denotations, while the code type and ExecFloat carrier remain executable. Define operation capabilities, exact observations, and conformance theorems separately.

source
def FloatLib.Numerics.floatFormatField :
Lean.ParserDescr

An assignment to Code, Scalar, or denote in a float_format declaration.

Instances For
    source
    def FloatLib.Numerics.floatFormatBody :
    Lean.ParserDescr

    Parsed body of a float_format declaration.

    Instances For
      source
      def FloatLib.Numerics.floatFormatDecl :
      Lean.ParserDescr

      Declare a static encoded numerical format and its denotation.

      Instances For