def Float.Model.UnpackedFloat.sqrtCore (spec : Format) (m : Nat) (e : Int) : Nat × Int × Accuracy

Computes a (mantissa, exponent) pair for the square root with enough bits to populate the mantissa for the given specification. Also returns an Accuracy stating how the returned pair relates to the infinitely precise square root.

def Float.Model.UnpackedFloat.sqrt (spec : Format) : UnpackedFloat → UnpackedFloat

Computes the square root of a floating-point number and rounds the result according to the given specification.