fact: Definition round_pos (rdir : rnd_record -> bool) (rexp : Z -> Z) (m : positive) (e : Z) := let e' := rexp (e + Zpos (digits m))%Z in match (e' - e)%Z with | Zpos d => let r := shr m d in ((if rdir r then N.succ (rnd_m r) else rnd_m r), e') | _ => (Npos m, e) end.
imports: Coq(Decidable Bool ZArith Reals Lia) Flocq(Core Bracket Digits) Gappa_definitions Gappa_dyadic Gappa_round_def Gappa_round_aux