# Documentation

## Batteries.Data.Nat.Basic

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

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

Equations
Instances For
@[irreducible]
def Nat.strongRec {motive : NatSort u_1} (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) (t : Nat) :
motive t

Strong recursor for Nat

Equations
Instances For
def Nat.strongRecOn (t : Nat) {motive : NatSort u_1} (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
motive t

Strong recursor for Nat

Equations
Instances For
@[irreducible]
def Nat.strongRecMeasure {α : Sort u_1} (f : αNat) {motive : αSort u_2} (ind : (x : α) → ((y : α) → f y < f xmotive y)motive x) (x : α) :
motive x

Strong recursor via a Nat-valued measure

Equations
Instances For
def Nat.recDiagAux {motive : NatNatSort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) (m : Nat) (n : Nat) :
motive m n

Simple diagonal recursor for Nat

Equations
Instances For
def Nat.recDiag {motive : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) (m : Nat) (n : Nat) :
motive m n

Diagonal recursor for Nat

Equations
Instances For
def Nat.recDiag.left {motive : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (n : Nat) :
motive 0 n

Left leg for Nat.recDiag

Equations
Instances For
def Nat.recDiag.right {motive : NatNatSort u_1} (zero_zero : motive 0 0) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (m : Nat) :
motive m 0

Right leg for Nat.recDiag

Equations
Instances For
def Nat.recDiagOn {motive : NatNatSort u_1} (m : Nat) (n : Nat) (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) :
motive m n

Diagonal recursor for Nat

Equations
Instances For
def Nat.casesDiagOn {motive : NatNatSort 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.
Instances For
def Nat.sum (l : ) :

Sum of a list of natural numbers.

Equations
Instances For
def Nat.sqrt (n : Nat) :

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

Equations
Instances For
@[irreducible]
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
Instances For