TorchLean API

Docs HomeGuideExamplesGraphs

NN.Floats.IEEEExec.Exec32.Instances

IEEE32 Executable Instances #

This file gives IEEE32Exec the standard Lean numeric interfaces needed by tensor specs and examples. The instances route arithmetic through the executable binary32 operations defined in the Exec32 hierarchy.

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instToString :
ToString IEEE32Exec

Pretty-print using Lean's Float printer (via toFloat).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instCoeNat :
Coe ℕ IEEE32Exec

Coerce naturals to binary32 by converting through Lean's Float and re-encoding.

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instOfNat (n : ℕ) :
OfNat IEEE32Exec n

Numeral literals for IEEE32Exec.

This allows writing:

  • (1 : IEEE32Exec)
  • (42 : IEEE32Exec)

The interpretation is Nat → Float (binary64) → IEEE32Exec via ofFloat, i.e. it rounds the exact integer to the nearest representable float32 (which is exact for small enough integers).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instZero :
Zero IEEE32Exec

0.0 as an executable binary32 value (chosen as +0.0).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instOne :
One IEEE32Exec

1.0 as an executable binary32 value.

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instNeg :
Neg IEEE32Exec

Unary negation (IEEE-754 sign flip, with NaN payload rules).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instAdd :
Add IEEE32Exec

IEEE-754 addition (with NaN/Inf rules).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instSub :
Sub IEEE32Exec

IEEE-754 subtraction (with NaN/Inf rules).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instMul :
Mul IEEE32Exec

IEEE-754 multiplication (with NaN/Inf rules).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instDiv :
Div IEEE32Exec

IEEE-754 division (with NaN/Inf rules).

source
@[implicit_reducible]
instance TorchLean.Floats.IEEE754.IEEE32Exec.instPow :
Pow IEEE32Exec IEEE32Exec

Exponentiation instance.

This is a deterministic executable choice, not a claim about correctly-rounded pow: we implement a small set of IEEE-like special cases and handle integer exponents exactly enough to avoid the most common footguns (negative bases, 0^0, 1^∞, etc.). For general non-integer exponents we fall back to exp (b * log a) on positive bases.

source
def TorchLean.Floats.IEEE754.IEEE32Exec.instPow.powNatLinear (a : IEEE32Exec) :
ℕ → IEEE32Exec
Instances For
    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instBEq :
    BEq IEEE32Exec

    Boolean equality with IEEE-754 NaN/zero conventions.

    • If either side is NaN, we return false.
    • If both are zeros (either sign), we return true.
    • Otherwise we compare raw bits.
    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instLT :
    LT IEEE32Exec

    Strict order instance, defined via IEEE32Exec.lt.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instLE :
    LE IEEE32Exec

    Non-strict order instance, defined via IEEE32Exec.le.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableRelLt :
    DecidableRel fun (x1 x2 : IEEE32Exec) => x1 < x2

    Decidable < inherited from the compare-based definition.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableRelLe :
    DecidableRel fun (x1 x2 : IEEE32Exec) => x1 ≤ x2

    Decidable ≤ inherited from the compare-based definition.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instMin :
    Min IEEE32Exec

    min operator, implemented by IEEE-754 minimum.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instMax :
    Max IEEE32Exec

    max operator, implemented by IEEE-754 maximum.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instMathFunctions :
    MathFunctions IEEE32Exec

    Provide the MathFunctions interface using the deterministic implementations in this file.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instNumbers :
    Numbers IEEE32Exec

    Numeric constants used by the spec library, instantiated at binary32.

    source
    @[implicit_reducible]
    instance TorchLean.Floats.IEEE754.IEEE32Exec.instContext :
    Context IEEE32Exec

    Context instance so the spec layer can execute with IEEE32Exec scalars.