def Nat.recAux {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (t : Nat) : motive t

Recursor identical to Nat.rec but uses notations 0 for Nat.zero and ·+1 for Nat.succ

Equations

• Nat.recAux zero succ 0 = zero
• Nat.recAux zero succ (Nat.succ n) = succ n (Nat.recAux zero succ n)

def Nat.recAuxOn {motive : Nat → Sort u_1} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : motive t

Recursor identical to Nat.recOn but uses notations 0 for Nat.zero and ·+1 for Nat.succ

Equations

• Nat.recAuxOn t zero succ = Nat.recAux zero succ t

def Nat.casesAuxOn {motive : Nat → Sort u_1} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : motive t

Recursor identical to Nat.casesOn but uses notations 0 for Nat.zero and ·+1 for Nat.succ

Equations

• Nat.casesAuxOn t zero succ = Nat.recAux zero (fun (n : Nat) (x : motive n) => succ n) t

def Nat.strongRec {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : motive t

Strong recursor for Nat

Equations

• Nat.strongRec ind t = ind t fun (m : Nat) (x : m < t) => Nat.strongRec ind m

def Nat.strongRecOn (t : Nat) {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) : motive t

Strong recursor for Nat

Equations

• Nat.strongRecOn t ind = Nat.strongRec ind t

def Nat.recDiagAux {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : motive m n

Simple diagonal recursor for Nat

Equations

• Nat.recDiagAux zero_left zero_right succ_succ 0 x = zero_left x
• Nat.recDiagAux zero_left zero_right succ_succ x 0 = zero_right x
• Nat.recDiagAux zero_left zero_right succ_succ (Nat.succ n) (Nat.succ n_1) = succ_succ n n_1 (Nat.recDiagAux zero_left zero_right succ_succ n n_1)

def Nat.recDiag {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : motive m n

Diagonal recursor for Nat

Equations

• Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n = Nat.recDiagAux (Nat.recDiag.left zero_zero zero_succ) (Nat.recDiag.right zero_zero succ_zero) succ_succ m n

def Nat.recDiag.left {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (n : Nat) : motive 0 n

Left leg for Nat.recDiag

Equations

• Nat.recDiag.left zero_zero zero_succ 0 = zero_zero
• Nat.recDiag.left zero_zero zero_succ (Nat.succ n) = zero_succ n (Nat.recDiag.left zero_zero zero_succ n)

def Nat.recDiag.right {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (m : Nat) : motive m 0

Right leg for Nat.recDiag

Equations

• Nat.recDiag.right zero_zero succ_zero 0 = zero_zero
• Nat.recDiag.right zero_zero succ_zero (Nat.succ n) = succ_zero n (Nat.recDiag.right zero_zero succ_zero n)

def Nat.recDiagOn {motive : Nat → Nat → Sort u_1} (m : Nat) (n : Nat) (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : motive m n

Diagonal recursor for Nat

Equations

• Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ = Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n

def Nat.casesDiagOn {motive : Nat → Nat → Sort u_1} (m : Nat) (n : Nat) (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) : motive m n

Diagonal recursor for Nat

Equations

• One or more equations did not get rendered due to their size.

instance Nat.instDvdNat : Dvd Nat

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

Equations

• Nat.instDvdNat = { dvd := fun (a b : Nat) => ∃ (c : Nat), b = a * c }

def Nat.lcm (m : Nat) (n : Nat) : Nat

The least common multiple of m and n, defined using gcd.

Equations

• Nat.lcm m n = m * n / Nat.gcd m n

def Nat.sum (l : List Nat) : Nat

Sum of a list of natural numbers.

Equations

• Nat.sum l = List.foldr (fun (x x_1 : Nat) => x + x_1) 0 l

def Nat.sqrt (n : Nat) : Nat

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

Equations

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

def Nat.sqrt.iter (n : Nat) (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

testBit

We define an operation for testing individual bits in the binary representation of a number.

def Nat.testBit (m : Nat) (n : Nat) : Bool

testBit m n returns whether the (n+1) least significant bit is 1 or 0

Equations

• Nat.testBit m n = (m >>> n &&& 1 != 0)