fact: Definition sqrt mode prec (f : type) := match f with | Fnan => f | Float m e => match mantissa_sign m with | Mzero => f | Mnumber true _ => Fnan | Mnumber false p => let d := mantissa_digits p in let prec := match exponent_cmp prec exponent_zero with Gt => prec | _ => exponent_one end in let s := exponent_sub (exponent_add prec prec) d in let s := match exponent_cmp s exponent_zero with Gt => s | _ => exponent_zero end in let (e', r) := exponent_div2_floor (exponent_sub e s) in let s := if r then exponent_add s exponent_one else s in let m := match exponent_cmp s exponent_zero with Gt => mantissa_shl p s | _ => p end in let (m', pos) := mantissa_sqrt m in round_aux mode prec false m' e' pos end end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig