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