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 uses the proved native-word integer-root dispatcher when the radicand fits in UInt64. Wider radicands retain Lean's arbitrary-precision implementation.

source
@[inline]
def FloatLib.Floats.Formats.BinaryInterchange.Model.NativeModelSqrt.sqrtCore (spec : Float.Model.Format) (mantissa : ℕ) (exponent : Int) :
ℕ × Int × 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