fact: Fixpoint compatible t := match t with | CInt _ | CBinFl _ _ | CVar _ => true | COp _ t1 t2 => andb (compatible t1) (compatible t2) | CNearbyint t | CTrunc t | CSqrt t => compatible t | CRnd md t => match md with mode_NA => false | _ => compatible t end | CLdexp _ _ => false end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr