P3109 conversion capabilities

The destination quantizer uses the exact rational scalar domain and the ProjectionPolicy context. Context-free conversion selects FloatLib's nearest-even, no-saturation policy. A conversion's (mode := ...) option takes a P3109 RoundingMode, as in x.cast (target := ExecFloat.P3109 .binary8p4se) (mode := .up).

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.P3109.Conversion.quantizer {format : Formats.P3109.Format} : Quantizer (P3109 format) ℚ

Every valid P3109 descriptor supports policy-aware exact-rational quantization.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.P3109.Conversion.defaultQuantizer {format : Formats.P3109.Format} : DefaultQuantizer (P3109 format) ℚ

Context-free P3109 conversion uses nearest-even rounding and no saturation request.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.P3109.Conversion.roundingModes {format : Formats.P3109.Format} : RoundingModes (P3109 format) Formats.P3109.RoundingMode

Conversions into a P3109 destination take a P3109 RoundingMode, nearest-even by default.

@[instance_reducible, inline]

instance FloatLib.Floats.ExecFloat.P3109.Conversion.modeContext {format : Formats.P3109.Format} (mode : Formats.P3109.RoundingMode) : ModeContext (P3109 format) ℚ mode

A conversion's (mode := m) selects rounding m with no saturation request. Passing (context := { rounding := m, saturation := s }) also chooses the saturation.

@[simp]

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.context_modeContext {format : Formats.P3109.Format} (mode : Formats.P3109.RoundingMode) : ModeContext.context = { rounding := mode }

The context a P3109 conversion's (mode := m) selects is { rounding := m }.