A recursor for Nat
that uses the notations 0
for Nat.zero
and n + 1
for Nat.succ
.
It is otherwise identical to the default recursor Nat.rec
. It is used by the induction
tactic
by default for Nat
.
Equations
Instances For
A case analysis principle for Nat
that uses the notations 0
for Nat.zero
and n + 1
for
Nat.succ
.
It is otherwise identical to the default recursor Nat.casesOn
. It is used as the default Nat
case analysis principle for Nat
by the cases
tactic.
Equations
Instances For
Applies a function to a starting value the specified number of times.
In other words, f
is iterated n
times on a
.
Examples:
Nat.repeat f 3 a = f <| f <| f <| a
Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"
Equations
Instances For
Applies a function to a starting value the specified number of times.
In other words, f
is iterated n
times on a
.
This is a tail-recursive version of Nat.repeat
that's used at runtime.
Examples:
Nat.repeatTR f 3 a = f <| f <| f <| a
Nat.repeatTR (· ++ "!") 4 "Hello" = "Hello!!!!"
Equations
Instances For
Equations
Instances For
The Boolean less-than comparison on natural numbers.
This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.
Examples: