Equations
- Nat.linearOrder = LinearOrder.mk Nat.le_total inferInstance inferInstance inferInstance
Equations
- Nat.strong_rec_on n H = WellFounded.fix' (_ : WellFounded WellFoundedRelation.rel) H n
Equations
- One or more equations did not get rendered due to their size.
bit0/bit1 properties
Equations
- Nat.two_step_induction H1 H2 H3 0 = H1
- Nat.two_step_induction H1 H2 H3 1 = H2
- Nat.two_step_induction H1 H2 H3 (Nat.succ (Nat.succ n)) = H3 n (Nat.two_step_induction H1 H2 H3 n) (Nat.two_step_induction H1 H2 H3 (Nat.succ n))
Equations
- Nat.sub_induction H1 H2 H3 0 x = H1 x
- Nat.sub_induction H1 H2 H3 (Nat.succ n) 0 = H2 n
- Nat.sub_induction H1 H2 H3 (Nat.succ n) (Nat.succ m) = H3 n m (Nat.sub_induction H1 H2 H3 n m)
Equations
- Nat.lt_by_cases h₁ h₂ h₃ = Nat.lt_ge_by_cases h₁ fun h₁ => Nat.lt_ge_by_cases h₃ fun h => h₂ (_ : a = b)
If p
is a (decidable) predicate on ℕ
and hp : ∃ (n : ℕ), p n∃ (n : ℕ), p n
is a proof that
there exists some natural number satisfying p
, then Nat.find hp
is the
smallest natural number satisfying p
. Note that Nat.find
is protected,
meaning that you can't just write find
, even if the Nat
namespace is open.
The API for Nat.find
is:
Nat.find_spec
is the proof thatNat.find hp
satisfiesp
.Nat.find_min
is the proof that ifm < Nat.find hp
thenm
does not satisfyp
.Nat.find_min'
is the proof that ifm
does satisfyp
thenNat.find hp ≤ m≤ m
.
The String representation produced by toDigitsCore has the proper length relative to
the number of digits in n < e
for some base b
. Since this works with any base greater
than one, it can be used for binary, decimal, and hex.
The core implementation of Nat.repr
returns a String with length less than or equal to the
number of digits in the decimal number (represented by e
). For example, the decimal string
representation of any number less than 1000 (10 ^ 3) has a length less than or equal to 3.