TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.Word.ModelSqrt.Runtime

Executable native-backed unpacked floating-point square root #

The unpacked-float square-root implementation reduces the radicand to the rounding scale before calling the proved integer-root dispatcher. The original core remains available with its exact logical-model contract.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeModelSqrt.sqrtCore (spec : Float.Model.Format) (mantissa : ℕ) (exponent : ℤ) :
ℕ × ℤ × Float.Model.UnpackedFloat.Accuracy

Native-backed implementation of Lean's unpacked square-root core.

Instances For
    source
    @[inline]
    def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeModelSqrt.sqrt (spec : Float.Model.Format) :
    Float.Model.UnpackedFloat → Float.Model.UnpackedFloat

    Native-backed implementation of Lean's logical unpacked floating-point square root.

    Instances For