fact: Definition nearbyint default (mode : rounding_mode) (f : type) := if real f then let '(f', e) := frshiftexp f in if Int63.leb (of_Z (FloatOps.prec + FloatOps.shift))%int63 e then f else let m := normfr_mantissa f' in let d := (of_Z (FloatOps.prec + FloatOps.shift) - e)%int63 in let mh := (m >> d)%int63 in match mode with | rnd_ZR => if get_sign f then (- (of_int63 mh))%float else of_int63 mh | rnd_DN => if get_sign f then let f'' := (- (of_int63 mh))%float in if PrimFloat.ltb f f'' then (- (of_int63 (mh + 1)))%float else f'' else of_int63 mh | rnd_UP => if get_sign f then PrimFloat.opp (of_int63 mh) else let f'' := of_int63 mh in if PrimFloat.ltb f'' f then of_int63 (mh + 1) else f'' | rnd_NE => let fl := of_int63 mh in let f' := match (abs f - fl ?= 0.5)%float with | FLt => fl | FGt => of_int63 (mh + 1) | FEq | FNotComparable => if Int63.eqb (mh land 1) 0 then fl else of_int63 (mh + 1) end in if get_sign f then (- f')%float else f' end else default.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig