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
Instances For
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
Instances For
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
Instances For
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
Instances For
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]
.