Documentation

Std.Data.Nat.Basic

instance Nat.instDvdNat :

Divisibility of natural numbers. a ∣ b∣ b (typed as \|) says that there is some c such that b = a * c.

Equations
def Nat.sum (l : ) :

Sum of a list of natural numbers.

Equations
def Nat.sqrt (n : Nat) :

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

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

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

Equations