Divisibility of natural numbers. a ∣ b
(typed as \|
) says that
there is some c
such that b = a * c
.
Equations
Division of natural numbers, discarding the remainder. Division by 0
returns 0
. Usually accessed
via the /
operator.
This operation is sometimes called “floor division.”
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
21 / 3 = 7
21 / 5 = 4
0 / 22 = 0
5 / 0 = 0
Equations
Instances For
An induction principle customized for reasoning about the recursion pattern of natural number division by iterated subtraction.
Equations
Instances For
Division of two divisible natural numbers. Division by 0
returns 0
.
This operation uses an optimized implementation, specialized for two divisible natural numbers.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
Nat.divExact 21 3 (by decide) = 7
Nat.divExact 0 22 (by decide) = 0
Nat.divExact 0 0 (by decide) = 0
Equations
Instances For
The modulo operator, which computes the remainder when dividing one natural number by another.
Usually accessed via the %
operator. When the divisor is 0
, the result is the dividend rather
than an error.
This is the core implementation of Nat.mod
. It computes the correct result for any two closed
natural numbers, but it does not have some convenient definitional
reductions when the Nat
s contain free variables. The wrapper
Nat.mod
handles those cases specially and then calls Nat.modCore
.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Equations
Instances For
The modulo operator, which computes the remainder when dividing one natural number by another.
Usually accessed via the %
operator. When the divisor is 0
, the result is the dividend rather
than an error.
Nat.mod
is a wrapper around Nat.modCore
that special-cases two situations, giving better
definitional reductions:
Nat.mod 0 m
should reduce tom
, for all termsm : Nat
.Nat.mod n (m + n + 1)
should reduce ton
for concreteNat
literalsn
.
These reductions help Fin n
literals work well, because the OfNat
instance for Fin
uses
Nat.mod
. In particular, (0 : Fin (n + 1)).val
should reduce definitionally to 0
. Nat.modCore
can handle all numbers, but its definitional reductions are not as convenient.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
7 % 2 = 1
9 % 3 = 0
5 % 7 = 5
5 % 0 = 5
show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl
show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl
Equations
Instances For
An induction principle customized for reasoning about the recursion pattern of Nat.mod
.