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

@[irreducible]

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

@[irreducible]

def Nat.strongRecMeasure {α : Sort u_1} (f : α → Nat) {motive : α → Sort u_2} (ind : (x : α) → ((y : α) → f y < f x → motive y) → motive x) (x : α) : motive x

Strong recursor via a Nat-valued measure

Equations

• Nat.strongRecMeasure f ind x = ind x fun (y : α) (x : f y < f x) => Nat.strongRecMeasure f ind y

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 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 n.succ n_1.succ = 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 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 n.succ = 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 n.succ = succ_zero n (Nat.recDiag.right zero_zero succ_zero n)

def Nat.recDiagOn {motive : Nat → Nat → Sort u_1} (m 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 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.

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 (n / 2)

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.

By default this well-founded recursion would be irreducible. This prevents use decide to resolve Nat.sqrt n for small values of n, so we mark this as @[semireducible].

Equations

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

@[inline]

def Nat.ofBits {n : Nat} (f : Fin n → Bool) : Nat

Construct a natural number from a sequence of bits using little endian convention.

Equations

• Nat.ofBits f = Fin.foldr n (fun (i : Fin n) (v : Nat) => 2 * v + (f i).toNat) 0