Format-generic executable exponential and logarithm

expWith and logWith execute against explicit approximation data. The convenience operations exp and log select Config.forFormat. Their finite results are deterministic approximations; accuracy bounds require separate certificates.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.atanhSeries (fixed : FixedPoint) (t : ℤ) (terms : ℕ) : ℤ

Evaluate the first terms terms of t + t^3/3 + t^5/5 + ... in a fixed-point context.

def FloatLib.Floats.Formats.BinaryInterchange.Model.expWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate exponential using a delayed configuration provider.

The provider is called only for a finite input, so generated configurations are not constructed for NaNs or infinities.

def FloatLib.Floats.Formats.BinaryInterchange.Model.logWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate logarithm using a delayed configuration provider.

The provider is called only for a finite positive input.

def FloatLib.Floats.Formats.BinaryInterchange.Model.expWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic exponential using range reduction and an explicit fixed-point polynomial.

NaNs are quieted and infinities use the destination format's native overflow and zero policies.

def FloatLib.Floats.Formats.BinaryInterchange.Model.logWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic natural logarithm using centered dyadic normalization and an odd atanh series.

Inputs near one use additional working precision and avoid a logarithmic subtraction. Special values follow the destination format's native overflow and invalid-result policies.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.exp {fmt : FloatFormat} (x : Model fmt) : Model fmt

Exponential using the default configuration for the destination format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.log {fmt : FloatFormat} (x : Model fmt) : Model fmt

Natural logarithm using the default configuration for the destination format.