Native-word integer square-root runtime #
Bounded integer square root uses an overflow-free average and Newton iteration. Its Nat.sqrt
refinement is isolated in IntegerSquareRoot.Proof.
@[inline]
Floor of the average of two native words, without overflowing their sum.
The low-bit conjunction supplies the carry exactly when both operands are odd.
Instances For
@[irreducible, inline]
Newton iteration for a native-word integer square root.
Instances For
@[inline]
Integer square root of one native word.
Instances For
@[inline]
Use the native-word square root for bounded natural numbers.
The arbitrary-precision branch repeats the logical definition so compiler simplification cannot recurse through the replacement theorem.