TorchLean API

FloatLib.Floats.Formats.FixedPoint.Bounded.Configured.Conversion.Instances

Bounded fixed-point conversion instances #

Bounded fixed-point destinations quantize exact rationals under a caller-chosen overflow policy. The context-free instance chooses .reject, as the arithmetic does.

@[instance_reducible]
instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.quantizer {radix : Numerics.Radix} {fractionalDigits width : ℕ} :
Quantizer (BoundedFixedPoint radix fractionalDigits width) ℚ

Bounded fixed-point conversion, with the overflow policy as its context.

@[instance_reducible]
instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.defaultQuantizer {radix : Numerics.Radix} {fractionalDigits width : ℕ} :
DefaultQuantizer (BoundedFixedPoint radix fractionalDigits width) ℚ

Context-free bounded conversion rejects overflow.