fact: Fixpoint wellFormed {Tl T} (t: ArithExpr Tl T) := match t with | Int _ n => (- Z.pow_pos 2 (Int32.bits - 1) <=? n)%Z && (n <? Z.pow_pos 2 (Int32.bits - 1))%Z | BinFl _ x => is_finite_SF (Prim2SF x) | Var _ _ => true | Op _ _ _ t1 t2 | OpExact _ _ t1 t2 => wellFormed t1 && wellFormed t2 | Fma _ t1 t2 t3 | FmaExact _ t1 t2 t3 => wellFormed t1 && wellFormed t2 && wellFormed t3 | Let _ _ _ t1 t2 => wellFormed t1 && wellFormed t2 | ArrayAcc _ a t => wellFormed t && finite_array a | Nearbyint _ t | FastNearbyint _ t | FastNearbyintToInt _ t | TruncToInt _ t | FloatInj _ t | Sqrt _ _ t | Assert _ _ _ t | Postcond _ _ _ t => wellFormed t end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)