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

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

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 x => 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

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

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

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

instance Nat.instDvdNat : Dvd Nat

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

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

Sum of a list of natural numbers.

def Nat.sqrt (n : Nat) : Nat

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

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