Explicit decimal rounding attributes and sticky exception flags

An arithmetic Outcome records the exceptions raised by one operation. An Environment accumulates those exceptions until a caller clears or restores the selected flags. Passing this state explicitly makes exception behavior available in pure Lean programs and proofs. Flag operations are defined in FloatLib.Numerics.IEEEStatus, shared with binary formats.

The flag operations implement the default-handling state of IEEE 754-2019 §§5.7.4 and 7. They do not change the host floating-point environment. A scoped rounding attribute changes the direction used inside a computation while preserving the exceptions raised there.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Exception : Type

The shared IEEE exception names, independent of radix and precision.

structure FloatLib.Floats.Formats.DecimalInterchange.Environment : Type

A decimal computation's explicit rounding direction and accumulated exception flags.

• rounding : RoundingMode

  The rounding direction used by computations in this environment.

• flags : Status

  Exceptions accumulated until explicitly cleared or restored.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqEnvironment : DecidableEq Environment

def FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqEnvironment.decEq (x✝ x✝¹ : Environment) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instReprEnvironment : Repr Environment

def FloatLib.Floats.Formats.DecimalInterchange.instReprEnvironment.repr : Environment → ℕ → Std.Format

def FloatLib.Floats.Formats.DecimalInterchange.Environment.raiseFlags (environment : Environment) (group : Status) : Environment

Set the selected sticky flags without changing the rounding direction.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.lowerFlags (environment : Environment) (group : Status) : Environment

Clear the selected sticky flags without changing the rounding direction.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.testFlags (environment : Environment) (group : Status) : Bool

Test whether any selected current flag is raised.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.saveAllFlags (environment : Environment) : Status

Save the current flags for a later test or restoration.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.restoreFlags (environment : Environment) (saved group : Status) : Environment

Restore selected flags from a saved snapshot, including saved clear flags.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.accept (environment : Environment) (outcome : Outcome) : Datum × Environment

Record an operation's result and accumulate its exceptions in the current flags.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.run (environment : Environment) (operation : RoundingMode → Outcome) : Datum × Environment

Evaluate one operation under the current rounding direction.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.withRounding {α : Type u_1} (environment : Environment) (rounding : RoundingMode) (computation : Environment → α × Environment) : α × Environment

Evaluate a computation under a scoped rounding direction. The outer direction is restored; the computation's final flags are preserved.