fact: Fixpoint assertions {Tl T} (t : ArithExpr Tl T) : evalExprTypeRounded_list Tl -> _ := match t with | Int _ _ | BinFl _ _ | Var _ _ | ArrayAcc _ _ _ => fun l md => True | Op _ _ _ t1 t2 | OpExact _ _ t1 t2 => fun l md => assertions t1 l md /\ assertions t2 l md | Fma _ t1 t2 t3 | FmaExact _ t1 t2 t3 => fun l md => assertions t1 l md /\ assertions t2 l md /\ assertions t3 l md | Nearbyint _ t | FastNearbyint _ t | FastNearbyintToInt _ t | TruncToInt _ t | FloatInj _ t | Sqrt _ _ t => fun l md => assertions t l md | Let _ _ _ t1 t2 => fun l md => assertions t1 l md /\ let x := evalRounded t1 l md in assertions t2 (x, l) md | Assert _ _ P t => fun l md => let P' := P (evalExact t l) in uncurrify P' l /\ assertions t l md | Postcond _ _ _ t => fun l md => assertions t l md end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)