fact: Definition convertibleFloat {T} : evalExprTypeFloat T -> Prop := match T with | Integer => fun n => Int32.in_bounds n | BinFloat => fun f => @is_finite Rrnd.prec Rrnd.emax f = true end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)