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 a natural number by rounding that exact integer directly to binary32.

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 conversion uses the exact dyadic n · 2⁰ and rounds once to nearest-even binary32. Avoiding an intermediate binary64 value prevents double rounding for large numerals.

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.

The value-level special cases follow the conventions used by common tensor runtimes:

x^(±0) = 1, including a NaN base;
1^y = 1 for finite, infinite, and quiet-NaN exponents (a signaling NaN still propagates);
an infinite exponent is classified from |x| relative to 1;
(-∞)^y has magnitude +∞ for positive finite y and +0 for negative finite y, with the usual signed result retained when y is an integer.

Finite negative bases accept integer exponents. For a general non-integer exponent on a positive base, the implementation falls back to exp (b * log a).

source