Posit quire inspection

#float_info shows the quire width, fixed-point scale, capacity, and exact accumulation operations. The quire has an exact source decoder and an explicit exit to its associated posit type. Its profile lists those operations separately from scalar ExecFloat arithmetic.

def FloatLib.Floats.Formats.Posit.Quire.FloatInfo.executionDeclarations : List Lean.Name

Quire conversion, capacity, and accumulation theorems shown by both posit reports.

def FloatLib.Floats.Formats.Posit.Quire.FloatInfo.profile (bits : ℕ) : ExecFloat.FormatProfile

Describe a Posit Standard (2022) quire and its operation contracts.