fact: Definition isConversionFloat {T} : evalExprTypeFloat T -> evalExprTypeRounded T -> Prop := match T with | Integer => fun n1 n2 => n1 = n2 | BinFloat => fun f r => @B2R Rrnd.prec Rrnd.emax f = r end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)