TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Logarithmic.Exact.Runtime

Exact logarithmic representation and execution #

A code is zero or a sign with an unbounded integer exponent at a fixed radix. This module keeps that representation, its executable rational decoder, and multiplication together. Multiplication handles zero, xors the signs, and adds the exponents; it introduces no rounding or overflow.

Exact.Proof supplies the real numerical system, erased proof views, and theorems connecting the rational decoder and multiplication kernel to their real semantics.

source
inductive FloatLib.Floats.Formats.Logarithmic.Code (radix : Numerics.Radix) :
Type

Exact logarithmic code at radix radix.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.Formats.Logarithmic.instDecidableEqCode {radix✝ : Numerics.Radix} :
    DecidableEq (Code radix✝)
    source
    def FloatLib.Floats.Formats.Logarithmic.instDecidableEqCode.decEq {radix✝ : Numerics.Radix} (x✝ x✝¹ : Code radix✝) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      def FloatLib.Floats.Formats.Logarithmic.instReprCode.repr {radix✝ : Numerics.Radix} :
      Code radix✝ → ℕ → Std.Format
      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.Logarithmic.instReprCode {radix✝ : Numerics.Radix} :
        Repr (Code radix✝)

        Executable operations #

        source
        def FloatLib.Floats.Formats.Logarithmic.Code.toRat {radix : Numerics.Radix} :
        Code radix → ℚ

        Exact rational value of a logarithmic code.

        Instances For
          source
          def FloatLib.Floats.Formats.Logarithmic.Code.mul {radix : Numerics.Radix} :
          Code radix → Code radix → Code radix

          Exact logarithmic multiplication.

          Instances For