fact: Definition P2M {T} : evalExprTypePrim T -> evalExprTypeRounded T := match T with | Integer => fun x => Sint63.to_Z x | BinFloat => fun x => SF2R radix2 (Prim2SF x) end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)