Executable numerical values

ExecFloat F stores a value in the code type chosen by format F. Formats provide arithmetic capabilities independently: notation and explicit calls such as ExecFloat.add use the same selected implementation. ExecFloat.Proof.*_eq_spec rewrites each operation to its reference definition in ExecFloat.Spec.

Conversions name the destination type. Mixed operations such as addAs name their result type; roundOnce evaluates a finite expression in that destination's exact domain and quantizes once.

Backend selection uses certified candidates and their cost estimates. #float_info reports the chosen implementation and available theorems. The directory README explains conversion, backend definitions, and generated-code checks. For runtime infrastructure without proof or inspection imports, use FloatLib.Floats.ExecFloat.Runtime.