fact: Definition convertiblePrim {T} : evalExprTypePrim T -> Prop := match T with | Integer => fun n => Int32.in_bounds (to_Z n) | BinFloat => fun f => @is_finite_SF (Prim2SF f) = true end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)