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. Because this state is an ordinary value, exception behavior is 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.

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

Rounding direction and accumulated exception flags of a decimal computation.

• rounding : RoundingMode

  The rounding direction used by computations in this environment.

• flags : Numerics.IEEEStatus

  Exceptions accumulated until a caller clears or restores them.

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

@[instance_reducible]

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

@[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 : Numerics.IEEEStatus) : Environment

Set the selected sticky flags without changing the rounding direction.

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

Clear the selected sticky flags without changing the rounding direction.

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

Test whether any selected current flag is raised.

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

Save the current flags for a later test or restoration.

def FloatLib.Floats.Formats.DecimalInterchange.Environment.restoreFlags (environment : Environment) (saved group : Numerics.IEEEStatus) : 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 and the computation's final flags are kept.