Documentation

Init.Data.Float.Model.Unpacked.Operations.Sqrt

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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.

    Equations
    Instances For