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

@[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

@[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

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

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

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

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

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

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

@[inline]

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

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

instance Nat.instNeZeroHPowOfNat_batteries {n : Nat} : NeZero (n ^ 0)