def Nat.sqrt (n : Nat) : Nat

Integer square root function. Implemented via Newton's method.

Equations

• n.sqrt = if n ≤ 1 then n else Nat.sqrt.iter n (1 <<< (n.log2 / 2 + 1))

@[irreducible]

def Nat.sqrt.iter (n guess : Nat) : Nat

Auxiliary for sqrt. If guess is greater than the integer square root of n, returns the integer square root of n.

Equations

• Nat.sqrt.iter n guess = if _h : (guess + n / guess) / 2 < guess then Nat.sqrt.iter n ((guess + n / guess) / 2) else guess