From cbfb9e482f1022dbe975ed48cb8da319210e9352 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 20 Mar 2025 10:13:36 +0100 Subject: [PATCH] doc: review of Nat docstrings (#7552) This PR adds missing `Nat` docstrings and makes their style consistent. --------- Co-authored-by: Bhavik Mehta --- src/Init/Data/Nat/Basic.lean | 72 ++++++-- src/Init/Data/Nat/Bitwise/Basic.lean | 50 +++++- src/Init/Data/Nat/Bitwise/Lemmas.lean | 5 +- src/Init/Data/Nat/Control.lean | 51 ++++++ src/Init/Data/Nat/Div/Basic.lean | 63 ++++++- src/Init/Data/Nat/Fold.lean | 75 +++++++- src/Init/Data/Nat/Gcd.lean | 25 ++- src/Init/Data/Nat/Lcm.lean | 11 +- src/Init/Data/Nat/Log2.lean | 13 +- src/Init/Data/Nat/Power2.lean | 13 ++ src/Init/Data/OfScientific.lean | 10 +- src/Init/Data/Repr.lean | 74 ++++++++ src/Init/Data/SInt/Basic.lean | 87 ++++++++- src/Init/Data/UInt/BasicAux.lean | 80 ++++++++- src/Init/Prelude.lean | 168 ++++++++++-------- src/Init/WF.lean | 9 + .../lean/interactive/hover.lean.expected.out | 18 +- .../interactive/hoverDot.lean.expected.out | 8 +- 18 files changed, 696 insertions(+), 136 deletions(-) diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean index c8df802ac3..47c0f6528c 100644 --- a/src/Init/Data/Nat/Basic.lean +++ b/src/Init/Data/Nat/Basic.lean @@ -23,35 +23,69 @@ private theorem rec_eq_recCompiled : @Nat.rec = @Nat.recCompiled := funext fun _ => funext fun _ => funext fun succ => funext fun t => Nat.recOn t rfl (fun n ih => congrArg (succ n) ih) -/-- Recursor identical to `Nat.rec` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`. -Used as the default `Nat` eliminator by the `induction` tactic. -/ +/-- +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`. +-/ @[elab_as_elim, induction_eliminator] protected abbrev recAux {motive : Nat → Sort u} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (t : Nat) : motive t := Nat.rec zero succ t -/-- Recursor identical to `Nat.casesOn` but uses notations `0` for `Nat.zero` and `· + 1` for `Nat.succ`. -Used as the default `Nat` eliminator by the `cases` tactic. -/ +/-- +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. +-/ @[elab_as_elim, cases_eliminator] protected abbrev casesAuxOn {motive : Nat → Sort u} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : motive t := Nat.casesOn t zero succ /-- -`Nat.repeat f n a` is `f^(n) a`; that is, it iterates `f` `n` times on `a`. +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!!!!"` -/ @[specialize] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α | 0, a => a | succ n, a => f (repeat f n a) -/-- Tail-recursive version of `Nat.repeat`. -/ +/-- +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!!!!"` +-/ @[inline] def repeatTR {α : Type u} (f : α → α) (n : Nat) (a : α) : α := let rec @[specialize] loop | 0, a => a | succ n, a => loop n (f a) loop n a -/-- Boolean less-than of natural numbers. -/ +/-- +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: + * `Nat.blt 2 5 = true` + * `Nat.blt 5 2 = false` + * `Nat.blt 5 5 = false` +-/ def blt (a b : Nat) : Bool := ble a.succ b @@ -785,9 +819,15 @@ instance {n m : Nat} [NeZero n] : NeZero (n^m) := /-! # min/max -/ /-- -`Nat.min a b` is the minimum of `a` and `b`: -* if `a ≤ b` then `Nat.min a b = a` -* if `b ≤ a` then `Nat.min a b = b` +Returns the lesser of two natural numbers. Usually accessed via `Min.min`. + +Returns `n` if `n ≤ m`, or `m` if `m ≤ n`. + +Examples: +* `min 0 5 = 0` +* `min 4 5 = 4` +* `min 4 3 = 3` +* `min 8 8 = 8` -/ protected abbrev min (n m : Nat) := min n m @@ -796,9 +836,15 @@ protected theorem min_def {n m : Nat} : min n m = if n ≤ m then n else m := rf instance : Max Nat := maxOfLe /-- -`Nat.max a b` is the maximum of `a` and `b`: -* if `a ≤ b` then `Nat.max a b = b` -* if `b ≤ a` then `Nat.max a b = a` +Returns the greater of two natural numbers. Usually accessed via `Max.max`. + +Returns `m` if `n ≤ m`, or `n` if `m ≤ n`. + +Examples: +* `max 0 5 = 5` +* `max 4 5 = 5` +* `max 4 3 = 4` +* `max 8 8 = 8` -/ protected abbrev max (n m : Nat) := max n m diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean index 6de9522410..1dead23820 100644 --- a/src/Init/Data/Nat/Bitwise/Basic.lean +++ b/src/Init/Data/Nat/Bitwise/Basic.lean @@ -13,6 +13,12 @@ namespace Nat theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n := Nat.div_lt_self (Nat.zero_lt_of_ne_zero hNe) (Nat.lt_succ_self _) +/-- +A helper for implementing bitwise operators on `Nat`. + +Each bit of the resulting `Nat` is the result of applying `f` to the corresponding bits of the input +`Nat`s, up to the position of the highest set bit in either input. +-/ def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat := if n = 0 then if f false true then m else 0 @@ -30,16 +36,56 @@ def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat := r+r decreasing_by apply bitwise_rec_lemma; assumption +/-- +Bitwise and. Usually accessed via the `&&&` operator. + +Each bit of the resulting value is set if the corresponding bit is set in both of the inputs. +-/ @[extern "lean_nat_land"] def land : @& Nat → @& Nat → Nat := bitwise and + +/-- +Bitwise or. Usually accessed via the `|||` operator. + +Each bit of the resulting value is set if the corresponding bit is set in at least one of the inputs. +-/ @[extern "lean_nat_lor"] def lor : @& Nat → @& Nat → Nat := bitwise or + +/-- +Bitwise exclusive or. Usually accessed via the `^^^` operator. + +Each bit of the resulting value is set if the corresponding bit is set in exactly one of the inputs. +-/ @[extern "lean_nat_lxor"] def xor : @& Nat → @& Nat → Nat := bitwise bne + +/-- +Shifts the binary representation of a value left by the specified number of bits. Usually accessed +via the `<<<` operator. + +Examples: + * `1 <<< 2 = 4` + * `1 <<< 3 = 8` + * `0 <<< 3 = 0` + * `0xf1 <<< 4 = 0xf10` +-/ @[extern "lean_nat_shiftl"] def shiftLeft : @& Nat → @& Nat → Nat | n, 0 => n | n, succ m => shiftLeft (2*n) m + +/-- +Shifts the binary representation of a value right by the specified number of bits. Usually accessed +via the `>>>` operator. + +Examples: + * `4 >>> 2 = 1` + * `8 >>> 2 = 2` + * `8 >>> 3 = 1` + * `0 >>> 3 = 0` + * `0xf13a >>> 8 = 0xf1` +-/ @[extern "lean_nat_shiftr"] def shiftRight : @& Nat → @& Nat → Nat | n, 0 => n @@ -84,7 +130,9 @@ We define an operation for testing individual bits in the binary representation of a number. -/ -/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/ +/-- +Returns `true` if the `(n+1)`th least significant bit is `1`, or `false` if it is `0`. +-/ def testBit (m n : Nat) : Bool := -- `1 &&& n` is faster than `n &&& 1` for big `n`. 1 &&& (m >>> n) != 0 diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean index dcffc4bee2..852939e129 100644 --- a/src/Init/Data/Nat/Bitwise/Lemmas.lean +++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean @@ -36,7 +36,10 @@ private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 := /-! ### Preliminaries -/ /-- -An induction principal that works on division by two. +An induction principle for the natural numbers with two cases: + * `n = 0`, and the motive is satisfied for `0` + * `n > 0`, and the motive should be satisfied for `n` on the assumption that it is satisfied for + `n / 2`. -/ noncomputable def div2Induction {motive : Nat → Sort u} (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by diff --git a/src/Init/Data/Nat/Control.lean b/src/Init/Data/Nat/Control.lean index a0928496c5..187b78e9d7 100644 --- a/src/Init/Data/Nat/Control.lean +++ b/src/Init/Data/Nat/Control.lean @@ -8,33 +8,79 @@ import Init.Control.Basic import Init.Data.Nat.Basic import Init.Omega +set_option linter.missingDocs true + namespace Nat universe u v +/-- +Executes a monadic action on all the numbers less than some bound, in increasing order. + +Example: +````lean example +#eval Nat.forM 5 fun i _ => IO.println i +```` +````output +0 +1 +2 +3 +4 +```` +-/ @[inline] def forM {m} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) : m Unit := let rec @[specialize] loop : ∀ i, i ≤ n → m Unit | 0, _ => pure () | i+1, h => do f (n-i-1) (by omega); loop i (Nat.le_of_succ_le h) loop n (by simp) +/-- +Executes a monadic action on all the numbers less than some bound, in decreasing order. + +Example: +````lean example +#eval Nat.forRevM 5 fun i _ => IO.println i +```` +````output +4 +3 +2 +1 +0 +```` +-/ @[inline] def forRevM {m} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) : m Unit := let rec @[specialize] loop : ∀ i, i ≤ n → m Unit | 0, _ => pure () | i+1, h => do f i (by omega); loop i (Nat.le_of_succ_le h) loop n (by simp) +/-- +Iterates the application of a monadic function `f` to a starting value `init`, `n` times. At each +step, `f` is applied to the current value and to the next natural number less than `n`, in +increasing order. +-/ @[inline] def foldM {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α := let rec @[specialize] loop : ∀ i, i ≤ n → α → m α | 0, h, a => pure a | i+1, h, a => f (n-i-1) (by omega) a >>= loop i (Nat.le_of_succ_le h) loop n (by omega) init +/-- +Iterates the application of a monadic function `f` to a starting value `init`, `n` times. At each +step, `f` is applied to the current value and to the next natural number less than `n`, in +decreasing order. +-/ @[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α := let rec @[specialize] loop : ∀ i, i ≤ n → α → m α | 0, h, a => pure a | i+1, h, a => f i (by omega) a >>= loop i (Nat.le_of_succ_le h) loop n (by omega) init +/-- +Checks whether the monadic predicate `p` returns `true` for all numbers less that the given bound. +Numbers are checked in increasing order until `p` returns false, after which no further are checked. +-/ @[inline] def allM {m} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) : m Bool := let rec @[specialize] loop : ∀ i, i ≤ n → m Bool | 0, _ => pure true @@ -44,6 +90,11 @@ universe u v | false => pure false loop n (by simp) +/-- +Checks whether there is some number less that the given bound for which the monadic predicate `p` +returns `true`. Numbers are checked in increasing order until `p` returns true, after which +no further are checked. +-/ @[inline] def anyM {m} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) : m Bool := let rec @[specialize] loop : ∀ i, i ≤ n → m Bool | 0, _ => pure false diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean index 555d661014..2e24e47375 100644 --- a/src/Init/Data/Nat/Div/Basic.lean +++ b/src/Init/Data/Nat/Div/Basic.lean @@ -24,6 +24,21 @@ theorem div_rec_fuel_lemma {x y fuel : Nat} (hy : 0 < y) (hle : y ≤ x) (hfuel x - y < fuel := Nat.lt_of_lt_of_le (div_rec_lemma ⟨hy, hle⟩) (Nat.le_of_lt_succ hfuel) +/-- +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` +-/ @[extern "lean_nat_div"] protected def div (x y : @& Nat) : Nat := if hy : 0 < y then @@ -71,6 +86,10 @@ theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 e next => simp only [false_and, ↓reduceIte, *] +/-- +An induction principle customized for reasoning about the recursion pattern of natural number +division by iterated subtraction. +-/ def div.inductionOn.{u} {motive : Nat → Nat → Sort u} (x y : Nat) @@ -108,6 +127,20 @@ theorem div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n := by have := Nat.add_le_of_le_sub hKN this exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this +/-- +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](lean-manual://section/type-system) 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. +-/ +@[extern "lean_nat_mod"] protected noncomputable def modCore (x y : Nat) : Nat := if hy : 0 < y then let rec @@ -155,13 +188,38 @@ protected theorem modCore_eq (x y : Nat) : Nat.modCore x y = simp only [false_and, ↓reduceIte, *] +/-- +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 to `m`, for all terms `m : Nat`. + * `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`. + +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` +-/ @[extern "lean_nat_mod"] protected def mod : @& Nat → @& Nat → Nat /- Nat.modCore is defined with fuel and thus does not reduce with open terms very well. Nevertheless it is desirable for trivial `Nat.mod` calculations, namely * `Nat.mod 0 m` for all `m` - * `Nat.mod n (m+n)` for concrete literals `n`, + * `Nat.mod n (m + n + 1)` for concrete literals `n`, to reduce definitionally. This property is desirable for `Fin n` literals, as it means `(ofNat 0 : Fin n).val = 0` by definition. @@ -189,6 +247,9 @@ protected theorem modCore_eq_mod (n m : Nat) : Nat.modCore n m = n % m := by theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by rw [←Nat.modCore_eq_mod, ←Nat.modCore_eq_mod, Nat.modCore_eq] +/-- +An induction principle customized for reasoning about the recursion pattern of `Nat.mod`. +-/ def mod.inductionOn.{u} {motive : Nat → Nat → Sort u} (x y : Nat) diff --git a/src/Init/Data/Nat/Fold.lean b/src/Init/Data/Nat/Fold.lean index 6ba639457d..018aa4dfe5 100644 --- a/src/Init/Data/Nat/Fold.lean +++ b/src/Init/Data/Nat/Fold.lean @@ -13,14 +13,30 @@ universe u namespace Nat /-- -`Nat.fold` evaluates `f` on the numbers up to `n` exclusive, in increasing order: -* `Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2` +Iterates the application of a function `f` to a starting value `init`, `n` times. At each step, `f` +is applied to the current value and to the next natural number less than `n`, in increasing order. + +Examples: +* `Nat.fold 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))` +* `Nat.fold 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]` +* `Nat.fold 0 (fun i _ xs => xs.push i) #[] = #[]` -/ @[specialize] def fold {α : Type u} : (n : Nat) → (f : (i : Nat) → i < n → α → α) → (init : α) → α | 0, f, a => a | succ n, f, a => f n (by omega) (fold n (fun i h => f i (by omega)) a) -/-- Tail-recursive version of `Nat.fold`. -/ + +/-- +Iterates the application of a function `f` to a starting value `init`, `n` times. At each step, `f` +is applied to the current value and to the next natural number less than `n`, in increasing order. + +This is a tail-recursive version of `Nat.fold` that's used at runtime. + +Examples: +* `Nat.foldTR 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))` +* `Nat.foldTR 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]` +* `Nat.foldTR 0 (fun i _ xs => xs.push i) #[] = #[]` +-/ @[inline] def foldTR {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α) (init : α) : α := let rec @[specialize] loop : ∀ j, j ≤ n → α → α | 0, h, a => a @@ -28,31 +44,72 @@ namespace Nat loop n (by omega) init /-- -`Nat.foldRev` evaluates `f` on the numbers up to `n` exclusive, in decreasing order: -* `Nat.foldRev f 3 init = f 0 <| f 1 <| f 2 <| init` +Iterates the application of a function `f` to a starting value `init`, `n` times. At each step, `f` +is applied to the current value and to the next natural number less than `n`, in decreasing order. + +Examples: +* `Nat.foldRev 3 f init = (f 0 (by simp) <| f 1 (by simp) <| f 2 (by simp) init)` +* `Nat.foldRev 4 (fun i _ xs => xs.push i) #[] = #[3, 2, 1, 0]` +* `Nat.foldRev 0 (fun i _ xs => xs.push i) #[] = #[]` -/ @[specialize] def foldRev {α : Type u} : (n : Nat) → (f : (i : Nat) → i < n → α → α) → (init : α) → α | 0, f, a => a | succ n, f, a => foldRev n (fun i h => f i (by omega)) (f n (by omega) a) -/-- `any f n = true` iff there is `i in [0, n-1]` s.t. `f i = true` -/ +/-- +Checks whether there is some number less that the given bound for which `f` returns `true`. + +Examples: + * `Nat.any 4 (fun i _ => i < 5) = true` + * `Nat.any 7 (fun i _ => i < 5) = true` + * `Nat.any 7 (fun i _ => i % 2 = 0) = true` + * `Nat.any 1 (fun i _ => i % 2 = 1) = false` +-/ @[specialize] def any : (n : Nat) → (f : (i : Nat) → i < n → Bool) → Bool | 0, f => false | succ n, f => any n (fun i h => f i (by omega)) || f n (by omega) -/-- Tail-recursive version of `Nat.any`. -/ +/-- +Checks whether there is some number less that the given bound for which `f` returns `true`. + +This is a tail-recursive equivalent of `Nat.any` that's used at runtime. + +Examples: + * `Nat.anyTR 4 (fun i _ => i < 5) = true` + * `Nat.anyTR 7 (fun i _ => i < 5) = true` + * `Nat.anyTR 7 (fun i _ => i % 2 = 0) = true` + * `Nat.anyTR 1 (fun i _ => i % 2 = 1) = false` +-/ @[inline] def anyTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool := let rec @[specialize] loop : (i : Nat) → i ≤ n → Bool | 0, h => false | succ m, h => f (n - succ m) (by omega) || loop m (by omega) loop n (by omega) -/-- `all f n = true` iff every `i in [0, n-1]` satisfies `f i = true` -/ +/-- +Checks whether `f` returns `true` for every number strictly less than a bound. + +Examples: + * `Nat.all 4 (fun i _ => i < 5) = true` + * `Nat.all 7 (fun i _ => i < 5) = false` + * `Nat.all 7 (fun i _ => i % 2 = 0) = false` + * `Nat.all 1 (fun i _ => i % 2 = 0) = true` +-/ @[specialize] def all : (n : Nat) → (f : (i : Nat) → i < n → Bool) → Bool | 0, f => true | succ n, f => all n (fun i h => f i (by omega)) && f n (by omega) -/-- Tail-recursive version of `Nat.all`. -/ +/-- +Checks whether `f` returns `true` for every number strictly less than a bound. + +This is a tail-recursive equivalent of `Nat.all` that's used at runtime. + +Examples: + * `Nat.allTR 4 (fun i _ => i < 5) = true` + * `Nat.allTR 7 (fun i _ => i < 5) = false` + * `Nat.allTR 7 (fun i _ => i % 2 = 0) = false` + * `Nat.allTR 1 (fun i _ => i % 2 = 0) = true` +-/ @[inline] def allTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool := let rec @[specialize] loop : (i : Nat) → i ≤ n → Bool | 0, h => true diff --git a/src/Init/Data/Nat/Gcd.lean b/src/Init/Data/Nat/Gcd.lean index 4433b9fb19..08a4e81b3a 100644 --- a/src/Init/Data/Nat/Gcd.lean +++ b/src/Init/Data/Nat/Gcd.lean @@ -11,22 +11,19 @@ import Init.RCases namespace Nat /-- -Computes the greatest common divisor of two natural numbers. +Computes the greatest common divisor of two natural numbers. The GCD of two natural numbers is the +largest natural number that evenly divides both. -This reference implementation via the Euclidean algorithm -is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). -The definition provided here is the logical model -(and it is soundness-critical that they coincide). +In particular, the GCD of a number and `0` is the number itself. -The GCD of two natural numbers is the largest natural number -that divides both arguments. -In particular, the GCD of a number and `0` is the number itself: -``` -example : Nat.gcd 10 15 = 5 := rfl -example : Nat.gcd 0 5 = 5 := rfl -example : Nat.gcd 7 0 = 7 := rfl -``` +This reference implementation via the Euclidean algorithm is overridden in both the kernel and the +compiler to efficiently evaluate using arbitrary-precision arithmetic. The definition provided here +is the logical model. + +Examples: +* `Nat.gcd 10 15 = 5` +* `Nat.gcd 0 5 = 5` +* `Nat.gcd 7 0 = 7` -/ @[extern "lean_nat_gcd"] def gcd (m n : @& Nat) : Nat := diff --git a/src/Init/Data/Nat/Lcm.lean b/src/Init/Data/Nat/Lcm.lean index a9c92bbfb0..1a9688d86f 100644 --- a/src/Init/Data/Nat/Lcm.lean +++ b/src/Init/Data/Nat/Lcm.lean @@ -17,7 +17,16 @@ that should be added to this file. namespace Nat -/-- The least common multiple of `m` and `n`, defined using `gcd`. -/ +/-- +The least common multiple of `m` and `n` is the smallest natural number that's evenly divisible by +both `m` and `n`. Returns `0` if either `m` or `n` is `0`. + +Examples: + * `Nat.lcm 9 6 = 18` + * `Nat.lcm 9 3 = 9` + * `Nat.lcm 0 3 = 0` + * `Nat.lcm 3 0 = 0` +-/ def lcm (m n : Nat) : Nat := m * n / gcd m n theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by diff --git a/src/Init/Data/Nat/Log2.lean b/src/Init/Data/Nat/Log2.lean index ff85ddb6f0..6bf217e3b3 100644 --- a/src/Init/Data/Nat/Log2.lean +++ b/src/Init/Data/Nat/Log2.lean @@ -18,9 +18,18 @@ theorem log2_terminates : ∀ n, n ≥ 2 → n / 2 < n simp /-- -Computes `⌊max 0 (log₂ n)⌋`. +Base-two logarithm of natural numbers. Returns `⌊max 0 (log₂ n)⌋`. -`log2 0 = log2 1 = 0`, `log2 2 = 1`, ..., `log2 (2^i) = i`, etc. +This function is overridden at runtime with an efficient implementation. This definition is +the logical model. + +Examples: + * `Nat.log2 0 = 0` + * `Nat.log2 1 = 0` + * `Nat.log2 2 = 1` + * `Nat.log2 4 = 2` + * `Nat.log2 7 = 2` + * `Nat.log2 8 = 3` -/ @[extern "lean_nat_log2"] def log2 (n : @& Nat) : Nat := diff --git a/src/Init/Data/Nat/Power2.lean b/src/Init/Data/Nat/Power2.lean index 4851d87edb..bfdc58961a 100644 --- a/src/Init/Data/Nat/Power2.lean +++ b/src/Init/Data/Nat/Power2.lean @@ -13,6 +13,16 @@ theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) rw [this, Nat.sub_add_eq] exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁ +/-- +Returns the least power of two that's greater than or equal to `n`. + +Examples: + * `Nat.nextPowerOfTwo 0 = 1` + * `Nat.nextPowerOfTwo 1 = 1` + * `Nat.nextPowerOfTwo 2 = 2` + * `Nat.nextPowerOfTwo 3 = 4` + * `Nat.nextPowerOfTwo 5 = 8` +-/ def nextPowerOfTwo (n : Nat) : Nat := go 1 (by decide) where @@ -24,6 +34,9 @@ where termination_by n - power decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption +/-- +A natural number `n` is a power of two if there exists some `k : Nat` such that `n = 2 ^ k`. +-/ def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k theorem isPowerOfTwo_one : isPowerOfTwo 1 := diff --git a/src/Init/Data/OfScientific.lean b/src/Init/Data/OfScientific.lean index 265b3d1dcc..01b7b51c26 100644 --- a/src/Init/Data/OfScientific.lean +++ b/src/Init/Data/OfScientific.lean @@ -45,6 +45,9 @@ protected opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float := instance : OfScientific Float where ofScientific := Float.ofScientific +/-- +Converts a natural number into a 64-bit floating point number. +-/ @[export lean_float_of_nat] def Float.ofNat (n : Nat) : Float := OfScientific.ofScientific n false 0 @@ -55,7 +58,7 @@ def Float.ofInt : Int → Float instance : OfNat Float n := ⟨Float.ofNat n⟩ -abbrev Nat.toFloat (n : Nat) : Float := +@[inherit_doc Float.ofNat] abbrev Nat.toFloat (n : Nat) : Float := Float.ofNat n /-- Computes `m * 2^e`. -/ @@ -76,6 +79,9 @@ protected opaque Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32 : instance : OfScientific Float32 where ofScientific := Float32.ofScientific +/-- +Converts a natural number into a 32-bit floating point number. +-/ @[export lean_float32_of_nat] def Float32.ofNat (n : Nat) : Float32 := OfScientific.ofScientific n false 0 @@ -86,5 +92,5 @@ def Float32.ofInt : Int → Float32 instance : OfNat Float32 n := ⟨Float32.ofNat n⟩ -abbrev Nat.toFloat32 (n : Nat) : Float32 := +@[inherit_doc Float32.ofNat] abbrev Nat.toFloat32 (n : Nat) : Float32 := Float32.ofNat n diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index be7980ec16..1eabb74955 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -129,6 +129,17 @@ We have pure functions for calculating the decimal representation of a `Nat` (`t a fast variant that handles small numbers (`USize`) via C code (`lean_string_of_usize`). -/ +/-- +Returns a single digit representation of `n`, which is assumed to be in a base less than or equal to +`16`. Returns `'*'` if `n > 15`. + +Examples: + * `Nat.digitChar 5 = '5'` + * `Nat.digitChar 12 = 'c'` + * `Nat.digitChar 15 = 'f'` + * `Nat.digitChar 16 = '*'` + * `Nat.digitChar 85 = '*'` +-/ def digitChar (n : Nat) : Char := if n = 0 then '0' else if n = 1 then '1' else @@ -156,6 +167,16 @@ def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char if n' = 0 then d::ds else toDigitsCore base fuel n' (d::ds) +/-- +Returns the decimal representation of a natural number as a list of digit characters in the given +base. If the base is greater than `16` then `'*'` is returned for digits greater than `0xf`. + +Examples: +* `Nat.toDigits 10 0xff = ['2', '5', '5']` +* `Nat.toDigits 8 0xc = ['1', '4']` +* `Nat.toDigits 16 0xcafe = ['c', 'a', 'f', 'e']` +* `Nat.toDigits 80 200 = ['2', '*']` +-/ def toDigits (base : Nat) (n : Nat) : List Char := toDigitsCore base (n+1) n [] @@ -172,10 +193,22 @@ private def reprFast (n : Nat) : String := if h : n < USize.size then (USize.ofNatLT n h).repr else (toDigits 10 n).asString +/-- +Converts a natural number to its decimal string representation. +-/ @[implemented_by reprFast] protected def repr (n : Nat) : String := (toDigits 10 n).asString +/-- +Converts a natural number less than `10` to the corresponding Unicode superscript digit character. +Returns `'*'` for other numbers. + +Examples: +* `Nat.superDigitChar 3 = '³'` +* `Nat.superDigitChar 7 = '⁷'` +* `Nat.superDigitChar 10 = '*'` +-/ def superDigitChar (n : Nat) : Char := if n = 0 then '⁰' else if n = 1 then '¹' else @@ -196,12 +229,37 @@ partial def toSuperDigitsAux : Nat → List Char → List Char if n' = 0 then d::ds else toSuperDigitsAux n' (d::ds) +/-- +Converts a natural number to the list of Unicode superscript digit characters that corresponds to +its decimal representation. + +Examples: + * `Nat.toSuperDigits 0 = ['⁰']` + * `Nat.toSuperDigits 35 = ['³', '⁵']` +-/ def toSuperDigits (n : Nat) : List Char := toSuperDigitsAux n [] +/-- +Converts a natural number to a string that contains the its decimal representation as Unicode +superscript digit characters. + +Examples: + * `Nat.toSuperscriptString 0 = "⁰"` + * `Nat.toSuperscriptString 35 = "³⁵"` +-/ def toSuperscriptString (n : Nat) : String := (toSuperDigits n).asString +/-- +Converts a natural number less than `10` to the corresponding Unicode subscript digit character. +Returns `'*'` for other numbers. + +Examples: +* `Nat.subDigitChar 3 = '₃'` +* `Nat.subDigitChar 7 = '₇'` +* `Nat.subDigitChar 10 = '*'` +-/ def subDigitChar (n : Nat) : Char := if n = 0 then '₀' else if n = 1 then '₁' else @@ -222,9 +280,25 @@ partial def toSubDigitsAux : Nat → List Char → List Char if n' = 0 then d::ds else toSubDigitsAux n' (d::ds) +/-- +Converts a natural number to the list of Unicode subscript digit characters that corresponds to +its decimal representation. + +Examples: + * `Nat.toSubDigits 0 = ['₀']` + * `Nat.toSubDigits 35 = ['₃', '₅']` +-/ def toSubDigits (n : Nat) : List Char := toSubDigitsAux n [] +/-- +Converts a natural number to a string that contains the its decimal representation as Unicode +subscript digit characters. + +Examples: + * `Nat.toSubscriptString 0 = "₀"` + * `Nat.toSubscriptString 35 = "₃₅"` +-/ def toSubscriptString (n : Nat) : String := (toSubDigits n).asString diff --git a/src/Init/Data/SInt/Basic.lean b/src/Init/Data/SInt/Basic.lean index 5f1975468e..e650c36b43 100644 --- a/src/Init/Data/SInt/Basic.lean +++ b/src/Init/Data/SInt/Basic.lean @@ -86,9 +86,29 @@ theorem Int8.toBitVec.inj : {x y : Int8} → x.toBitVec = y.toBitVec → x = y def Int8.mk (i : UInt8) : Int8 := UInt8.toInt8 i @[extern "lean_int8_of_int"] def Int8.ofInt (i : @& Int) : Int8 := ⟨⟨BitVec.ofInt 8 i⟩⟩ +/-- +Converts a natural number to an 8-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Int8.ofNat 53 = 53` + * `Int8.ofNat 127 = 127` + * `Int8.ofNat 128 = -128` + * `Int8.ofNat 255 = -1` +-/ @[extern "lean_int8_of_nat"] def Int8.ofNat (n : @& Nat) : Int8 := ⟨⟨BitVec.ofNat 8 n⟩⟩ abbrev Int.toInt8 := Int8.ofInt +/-- +Converts a natural number to an 8-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Nat.toInt8 53 = 53` + * `Nat.toInt8 127 = 127` + * `Nat.toInt8 128 = -128` + * `Nat.toInt8 255 = -1` +-/ abbrev Nat.toInt8 := Int8.ofNat @[extern "lean_int8_to_int"] def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt @@ -228,9 +248,29 @@ theorem Int16.toBitVec.inj : {x y : Int16} → x.toBitVec = y.toBitVec → x = y def Int16.mk (i : UInt16) : Int16 := UInt16.toInt16 i @[extern "lean_int16_of_int"] def Int16.ofInt (i : @& Int) : Int16 := ⟨⟨BitVec.ofInt 16 i⟩⟩ +/-- +Converts a natural number to a 16-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Int16.ofNat 127 = 127` + * `Int16.ofNat 32767 = 32767` + * `Int16.ofNat 32768 = -32768` + * `Int16.ofNat 32770 = -32766` +-/ @[extern "lean_int16_of_nat"] def Int16.ofNat (n : @& Nat) : Int16 := ⟨⟨BitVec.ofNat 16 n⟩⟩ abbrev Int.toInt16 := Int16.ofInt +/-- +Converts a natural number to a 16-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Nat.toInt16 127 = 127` + * `Nat.toInt16 32767 = 32767` + * `Nat.toInt16 32768 = -32768` + * `Nat.toInt16 32770 = -32766` +-/ abbrev Nat.toInt16 := Int16.ofNat @[extern "lean_int16_to_int"] def Int16.toInt (i : Int16) : Int := i.toBitVec.toInt @@ -374,9 +414,29 @@ theorem Int32.toBitVec.inj : {x y : Int32} → x.toBitVec = y.toBitVec → x = y def Int32.mk (i : UInt32) : Int32 := UInt32.toInt32 i @[extern "lean_int32_of_int"] def Int32.ofInt (i : @& Int) : Int32 := ⟨⟨BitVec.ofInt 32 i⟩⟩ +/-- +Converts a natural number to a 32-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Int32.ofNat 127 = 127` + * `Int32.ofNat 32770 = 32770` + * `Int32.ofNat 2_147_483_647 = 2_147_483_647` + * `Int32.ofNat 2_147_483_648 = -2_147_483_648` +-/ @[extern "lean_int32_of_nat"] def Int32.ofNat (n : @& Nat) : Int32 := ⟨⟨BitVec.ofNat 32 n⟩⟩ abbrev Int.toInt32 := Int32.ofInt +/-- +Converts a natural number to a 32-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Nat.toInt32 127 = 127` + * `Nat.toInt32 32770 = 32770` + * `Nat.toInt32 2_147_483_647 = 2_147_483_647` + * `Nat.toInt32 2_147_483_648 = -2_147_483_648` +-/ abbrev Nat.toInt32 := Int32.ofNat @[extern "lean_int32_to_int"] def Int32.toInt (i : Int32) : Int := i.toBitVec.toInt @@ -524,9 +584,31 @@ theorem Int64.toBitVec.inj : {x y : Int64} → x.toBitVec = y.toBitVec → x = y def Int64.mk (i : UInt64) : Int64 := UInt64.toInt64 i @[extern "lean_int64_of_int"] def Int64.ofInt (i : @& Int) : Int64 := ⟨⟨BitVec.ofInt 64 i⟩⟩ +/-- +Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Int64.ofNat 127 = 127` + * `Int64.ofNat 2_147_483_648 = 2_147_483_648` + * `Int64.ofNat 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807` + * `Int64.ofNat 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808` + * `Int64.ofNat 18_446_744_073_709_551_618 = 0` +-/ @[extern "lean_int64_of_nat"] def Int64.ofNat (n : @& Nat) : Int64 := ⟨⟨BitVec.ofNat 64 n⟩⟩ abbrev Int.toInt64 := Int64.ofInt +/-- +Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on +overflow. + +Examples: + * `Nat.toInt64 127 = 127` + * `Nat.toInt64 2_147_483_648 = 2_147_483_648` + * `Nat.toInt64 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807` + * `Nat.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808` + * `Nat.toInt64 18_446_744_073_709_551_618 = 0` +-/ abbrev Nat.toInt64 := Int64.ofNat @[extern "lean_int64_to_int_sint"] def Int64.toInt (i : Int64) : Int := i.toBitVec.toInt @@ -678,10 +760,13 @@ theorem ISize.toBitVec.inj : {x y : ISize} → x.toBitVec = y.toBitVec → x = y def ISize.mk (i : USize) : ISize := USize.toISize i @[extern "lean_isize_of_int"] def ISize.ofInt (i : @& Int) : ISize := ⟨⟨BitVec.ofInt System.Platform.numBits i⟩⟩ +/-- +Converts a natural number to an `ISize`, wrapping around to negative numbers on overflow. +-/ @[extern "lean_isize_of_nat"] def ISize.ofNat (n : @& Nat) : ISize := ⟨⟨BitVec.ofNat System.Platform.numBits n⟩⟩ abbrev Int.toISize := ISize.ofInt -abbrev Nat.toISize := ISize.ofNat +@[inherit_doc ISize.ofNat] abbrev Nat.toISize := ISize.ofNat @[extern "lean_isize_to_int"] def ISize.toInt (i : ISize) : Int := i.toBitVec.toInt /-- diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean index 1a84a6d870..c0b3d03351 100644 --- a/src/Init/Data/UInt/BasicAux.lean +++ b/src/Init/Data/UInt/BasicAux.lean @@ -20,6 +20,17 @@ open Nat def UInt8.toFin (x : UInt8) : Fin UInt8.size := x.toBitVec.toFin @[deprecated UInt8.toFin (since := "2025-02-12"), inherit_doc UInt8.toFin] def UInt8.val (x : UInt8) : Fin UInt8.size := x.toFin + +/-- +Converts a natural number to an 8-bit unsigned integer, wrapping on overflow. + +Examples: + * `UInt8.ofNat 5 = 5` + * `UInt8.ofNat 255 = 255` + * `UInt8.ofNat 256 = 0` + * `UInt8.ofNat 259 = 3` + * `UInt8.ofNat 32770 = 2` +-/ @[extern "lean_uint8_of_nat"] def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨BitVec.ofNat 8 n⟩ /-- @@ -30,6 +41,17 @@ def UInt8.ofNatTruncate (n : Nat) : UInt8 := UInt8.ofNatLT n h else UInt8.ofNatLT (UInt8.size - 1) (by decide) + +/-- +Converts a natural number to an 8-bit unsigned integer, wrapping on overflow. + +Examples: + * `Nat.toUInt8 5 = 5` + * `Nat.toUInt8 255 = 255` + * `Nat.toUInt8 256 = 0` + * `Nat.toUInt8 259 = 3` + * `Nat.toUInt8 32770 = 2` +-/ abbrev Nat.toUInt8 := UInt8.ofNat @[extern "lean_uint8_to_nat"] def UInt8.toNat (n : UInt8) : Nat := n.toBitVec.toNat @@ -40,6 +62,16 @@ instance UInt8.instOfNat : OfNat UInt8 n := ⟨UInt8.ofNat n⟩ def UInt16.toFin (x : UInt16) : Fin UInt16.size := x.toBitVec.toFin @[deprecated UInt16.toFin (since := "2025-02-12"), inherit_doc UInt16.toFin] def UInt16.val (x : UInt16) : Fin UInt16.size := x.toFin + +/-- +Converts a natural number to a 16-bit unsigned integer, wrapping on overflow. + +Examples: + * `UInt16.ofNat 5 = 5` + * `UInt16.ofNat 255 = 255` + * `UInt16.ofNat 32770 = 32770` + * `UInt16.ofNat 65537 = 1` +-/ @[extern "lean_uint16_of_nat"] def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨BitVec.ofNat 16 n⟩ /-- @@ -50,6 +82,16 @@ def UInt16.ofNatTruncate (n : Nat) : UInt16 := UInt16.ofNatLT n h else UInt16.ofNatLT (UInt16.size - 1) (by decide) + +/-- +Converts a natural number to a 16-bit unsigned integer, wrapping on overflow. + +Examples: + * `Nat.toUInt16 5 = 5` + * `Nat.toUInt16 255 = 255` + * `Nat.toUInt16 32770 = 32770` + * `Nat.toUInt16 65537 = 1` +-/ abbrev Nat.toUInt16 := UInt16.ofNat @[extern "lean_uint16_to_nat"] def UInt16.toNat (n : UInt16) : Nat := n.toBitVec.toNat @@ -64,6 +106,15 @@ instance UInt16.instOfNat : OfNat UInt16 n := ⟨UInt16.ofNat n⟩ def UInt32.toFin (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin @[deprecated UInt32.toFin (since := "2025-02-12"), inherit_doc UInt32.toFin] def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin + +/-- +Converts a natural number to a 32-bit unsigned integer, wrapping on overflow. + +Examples: + * `UInt32.ofNat 5 = 5` + * `UInt32.ofNat 65539 = 65539` + * `UInt32.ofNat 4_294_967_299 = 3` +-/ @[extern "lean_uint32_of_nat"] def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩ @[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT] @@ -76,6 +127,14 @@ def UInt32.ofNatTruncate (n : Nat) : UInt32 := UInt32.ofNatLT n h else UInt32.ofNatLT (UInt32.size - 1) (by decide) +/-- +Converts a natural number to a 32-bit unsigned integer, wrapping on overflow. + +Examples: + * `Nat.toUInt32 5 = 5` + * `Nat.toUInt32 65_539 = 65_539` + * `Nat.toUInt32 4_294_967_299 = 3` +-/ abbrev Nat.toUInt32 := UInt32.ofNat @[extern "lean_uint32_to_uint8"] def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8 @@ -110,6 +169,15 @@ theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt def UInt64.toFin (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin @[deprecated UInt64.toFin (since := "2025-02-12"), inherit_doc UInt64.toFin] def UInt64.val (x : UInt64) : Fin UInt64.size := x.toFin +/-- +Converts a natural number to a 64-bit unsigned integer, wrapping on overflow. + +Examples: + * `UInt64.ofNat 5 = 5` + * `UInt64.ofNat 65539 = 65539` + * `UInt64.ofNat 4_294_967_299 = 4_294_967_299` + * `UInt64.ofNat 18_446_744_073_709_551_620 = 4` +-/ @[extern "lean_uint64_of_nat"] def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨BitVec.ofNat 64 n⟩ /-- @@ -120,6 +188,15 @@ def UInt64.ofNatTruncate (n : Nat) : UInt64 := UInt64.ofNatLT n h else UInt64.ofNatLT (UInt64.size - 1) (by decide) +/-- +Converts a natural number to a 64-bit unsigned integer, wrapping on overflow. + +Examples: + * `Nat.toUInt64 5 = 5` + * `Nat.toUInt64 65539 = 65539` + * `Nat.toUInt64 4_294_967_299 = 4_294_967_299` + * `Nat.toUInt64 18_446_744_073_709_551_620 = 4` +-/ abbrev Nat.toUInt64 := UInt64.ofNat @[extern "lean_uint64_to_nat"] def UInt64.toNat (n : UInt64) : Nat := n.toBitVec.toNat @@ -153,6 +230,7 @@ theorem usize_size_pos : 0 < USize.size := def USize.toFin (x : USize) : Fin USize.size := x.toBitVec.toFin @[deprecated USize.toFin (since := "2025-02-12"), inherit_doc USize.toFin] def USize.val (x : USize) : Fin USize.size := x.toFin +/-- Converts a natural number to a `USize`, wrapping on overflow. -/ @[extern "lean_usize_of_nat"] def USize.ofNat (n : @& Nat) : USize := ⟨BitVec.ofNat _ n⟩ /-- @@ -164,7 +242,7 @@ def USize.ofNatTruncate (n : Nat) : USize := USize.ofNatLT n h else USize.ofNatLT (USize.size - 1) (Nat.pred_lt (Nat.ne_zero_of_lt USize.size_pos)) -abbrev Nat.toUSize := USize.ofNat +@[inherit_doc USize.ofNat] abbrev Nat.toUSize := USize.ofNat @[extern "lean_usize_to_nat"] def USize.toNat (n : USize) : Nat := n.toBitVec.toNat @[extern "lean_usize_add"] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index c0757cf34c..4163a80a4f 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1121,47 +1121,26 @@ propositional connective is `Not : Prop → Prop`. export Bool (or and not) /-- -The type of natural numbers, starting at zero. It is defined as an -inductive type freely generated by "zero is a natural number" and -"the successor of a natural number is a natural number". +The natural numbers, starting at zero. -You can prove a theorem `P n` about `n : Nat` by `induction n`, which will -expect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming -a proof of `P i`. The same method also works to define functions by recursion -on natural numbers: induction and recursion are two expressions of the same -operation from Lean's point of view. - -``` -open Nat -example (n : Nat) : n < succ n := by - induction n with - | zero => - show 0 < 1 - decide - | succ i ih => -- ih : i < succ i - show succ i < succ (succ i) - exact Nat.succ_lt_succ ih -``` - -This type is special-cased by both the kernel and the compiler: -* The type of expressions contains "`Nat` literals" as a primitive constructor, - and the kernel knows how to reduce zero/succ expressions to nat literals. -* If implemented naively, this type would represent a numeral `n` in unary as a - linked list with `n` links, which is horribly inefficient. Instead, the - runtime itself has a special representation for `Nat` which stores numbers up - to 2^63 directly and larger numbers use an arbitrary precision "bignum" - library (usually [GMP](https://gmplib.org/)). +This type is special-cased by both the kernel and the compiler, and overridden with an efficient +implementation. Both use a fast arbitrary-precision arithmetic library (usually +[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed. -/ inductive Nat where - /-- `Nat.zero`, is the smallest natural number. This is one of the two - constructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of - `0 : Nat` or simply `0`, in order to remain compatible with the simp normal - form defined by `Nat.zero_eq`. -/ + /-- + Zero, the smallest natural number. + + Using `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the + [simp normal form](lean-manual://section/simp-normal-forms). + -/ | zero : Nat - /-- The successor function on natural numbers, `succ n = n + 1`. - This is one of the two constructors of `Nat`. Using `succ n` should usually - be avoided in favor of `n + 1`, in order to remain compatible with the simp - normal form defined by `Nat.succ_eq_add_one`. -/ + /-- + The successor of a natural number `n`. + + Using `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal + form](lean-manual://section/simp-normal-forms). + -/ | succ (n : Nat) : Nat instance : Inhabited Nat where @@ -1619,11 +1598,10 @@ class Membership (α : outParam (Type u)) (γ : Type v) where set_option bootstrap.genMatcherCode false in /-- -Addition of natural numbers. +Addition of natural numbers, typically used via the `+` operator. -This definition is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model (and it is soundness-critical that they coincide). +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. -/ @[extern "lean_nat_add"] protected def Nat.add : (@& Nat) → (@& Nat) → Nat @@ -1639,11 +1617,10 @@ attribute [match_pattern] Nat.add Add.add HAdd.hAdd Neg.neg Mul.mul HMul.hMul set_option bootstrap.genMatcherCode false in /-- -Multiplication of natural numbers. +Multiplication of natural numbers, usually accessed via the `*` operator. -This definition is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model (and it is soundness-critical that they coincide). +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. -/ @[extern "lean_nat_mul"] protected def Nat.mul : (@& Nat) → (@& Nat) → Nat @@ -1655,11 +1632,10 @@ instance instMulNat : Mul Nat where set_option bootstrap.genMatcherCode false in /-- -The power operation on natural numbers. +The power operation on natural numbers, usually accessed via the `^` operator. -This definition is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model. +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. -/ @[extern "lean_nat_pow"] protected def Nat.pow (m : @& Nat) : (@& Nat) → Nat @@ -1670,11 +1646,10 @@ instance instNatPowNat : NatPow Nat := ⟨Nat.pow⟩ set_option bootstrap.genMatcherCode false in /-- -(Boolean) equality of natural numbers. +Boolean equality of natural numbers, usually accessed via the `==` operator. -This definition is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model (and it is soundness-critical that they coincide). +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. -/ @[extern "lean_nat_dec_eq"] def Nat.beq : (@& Nat) → (@& Nat) → Bool @@ -1701,11 +1676,16 @@ theorem Nat.ne_of_beq_eq_false : {n m : Nat} → Eq (beq n m) false → Not (Eq Nat.noConfusion h₂ (fun h₂ => absurd h₂ (ne_of_beq_eq_false this)) /-- -A decision procedure for equality of natural numbers. +A decision procedure for equality of natural numbers, usually accessed via the `DecidableEq Nat` +instance. -This definition is overridden in the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model. +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: + * `Nat.decEq 5 5 = isTrue rfl` + * `(if 3 = 4 then "yes" else "no") = "no"` + * `show 12 = 12 by decide` -/ @[reducible, extern "lean_nat_dec_eq"] protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) := @@ -1717,11 +1697,15 @@ protected def Nat.decEq (n m : @& Nat) : Decidable (Eq n m) := set_option bootstrap.genMatcherCode false in /-- -The (Boolean) less-equal relation on natural numbers. +The Boolean less-than-or-equal-to comparison on natural numbers. -This definition is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model (and it is soundness-critical that they coincide). +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: + * `Nat.ble 2 5 = true` + * `Nat.ble 5 2 = false` + * `Nat.ble 5 5 = true` -/ @[extern "lean_nat_dec_le"] def Nat.ble : @& Nat → @& Nat → Bool @@ -1731,11 +1715,10 @@ def Nat.ble : @& Nat → @& Nat → Bool | succ n, succ m => ble n m /-- -An inductive definition of the less-equal relation on natural numbers, -characterized as the least relation `≤` such that `n ≤ n` and `n ≤ m → n ≤ m + 1`. +Non-strict, or weak, inequality of natural numbers, usually accessed via the `≤` operator. -/ protected inductive Nat.le (n : Nat) : Nat → Prop - /-- Less-equal is reflexive: `n ≤ n` -/ + /-- Non-strict inequality is reflexive: `n ≤ n` -/ | refl : Nat.le n n /-- If `n ≤ m`, then `n ≤ m + 1`. -/ | step {m} : Nat.le n m → Nat.le n (succ m) @@ -1743,7 +1726,11 @@ protected inductive Nat.le (n : Nat) : Nat → Prop instance instLENat : LE Nat where le := Nat.le -/-- The strict less than relation on natural numbers is defined as `n < m := n + 1 ≤ m`. -/ +/-- +Strict inequality of natural numbers, usually accessed via the `<` operator. + +It is defined as `n < m = n + 1 ≤ m`. +-/ protected def Nat.lt (n m : Nat) : Prop := Nat.le (succ n) m @@ -1792,10 +1779,11 @@ theorem Nat.succ_pos (n : Nat) : LT.lt 0 (succ n) := set_option bootstrap.genMatcherCode false in /-- -The predecessor function on natural numbers. +The predecessor of a natural number is one less than it. The precedessor of `0` is defined to be +`0`. -This definition is overridden in the compiler to use `n - 1` instead. -The definition provided here is the logical model. +This definition is overridden in the compiler with an efficient implementation. This definition is +the logical model. -/ @[extern "lean_nat_pred"] def Nat.pred : (@& Nat) → Nat @@ -1875,10 +1863,30 @@ theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true := theorem Nat.not_le_of_not_ble_eq_true (h : Not (Eq (Nat.ble n m) true)) : Not (LE.le n m) := fun h' => absurd (Nat.ble_eq_true_of_le h') h +/-- +A decision procedure for non-strict inequality of natural numbers, usually accessed via the +`DecidableLE Nat` instance. + +Examples: + * `(if 3 ≤ 4 then "yes" else "no") = "yes"` + * `(if 6 ≤ 4 then "yes" else "no") = "no"` + * `show 12 ≤ 12 by decide` + * `show 5 ≤ 12 by decide` +-/ @[extern "lean_nat_dec_le"] instance Nat.decLe (n m : @& Nat) : Decidable (LE.le n m) := dite (Eq (Nat.ble n m) true) (fun h => isTrue (Nat.le_of_ble_eq_true h)) (fun h => isFalse (Nat.not_le_of_not_ble_eq_true h)) +/-- +A decision procedure for strict inequality of natural numbers, usually accessed via the +`DecidableLT Nat` instance. + +Examples: + * `(if 3 < 4 then "yes" else "no") = "yes"` + * `(if 4 < 4 then "yes" else "no") = "no"` + * `(if 6 < 4 then "yes" else "no") = "no"` + * `show 5 < 12 by decide` +-/ @[extern "lean_nat_dec_lt"] instance Nat.decLt (n m : @& Nat) : Decidable (LT.lt n m) := decLe (succ n) m @@ -1887,12 +1895,18 @@ instance : Min Nat := minOfLe set_option bootstrap.genMatcherCode false in /-- -(Truncated) subtraction of natural numbers. Because natural numbers are not -closed under subtraction, we define `n - m` to be `0` when `n < m`. +Subtraction of natural numbers, truncated at `0`. Usually used via the `-` operator. -This definition is overridden in both the kernel and the compiler to efficiently -evaluate using the "bignum" representation (see `Nat`). The definition provided -here is the logical model (and it is soundness-critical that they coincide). +If a result would be less than zero, then the result is zero. + +This definition 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: +* `5 - 3 = 2` +* `8 - 2 = 6` +* `8 - 8 = 0` +* `8 - 20 = 0` -/ @[extern "lean_nat_sub"] protected def Nat.sub : (@& Nat) → (@& Nat) → Nat @@ -2293,15 +2307,15 @@ instance : Inhabited USize where default := USize.ofNatLT 0 USize.size_pos /-- -A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and -it is also not a "surrogate" character (the range `0xd800` to `0xdfff` inclusive). +A `Nat` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a +surrogate code point (the range `0xd800` to `0xdfff` inclusive). -/ abbrev Nat.isValidChar (n : Nat) : Prop := Or (LT.lt n 0xd800) (And (LT.lt 0xdfff n) (LT.lt n 0x110000)) /-- -A `UInt32` denotes a valid unicode codepoint if it is less than `0x110000`, and -it is also not a "surrogate" character (the range `0xd800` to `0xdfff` inclusive). +A `UInt32` denotes a valid Unicode code point if it is less than `0x110000` and it is also not a +surrogate code point (the range `0xd800` to `0xdfff` inclusive). -/ abbrev UInt32.isValidChar (n : UInt32) : Prop := n.toNat.isValidChar diff --git a/src/Init/WF.lean b/src/Init/WF.lean index 52490a5f57..10c0f52ea8 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -189,12 +189,21 @@ def lt_wfRel : WellFoundedRelation Nat where | Or.inl e => subst e; assumption | Or.inr e => exact Acc.inv ih e +/-- +Strong induction on the natural numbers. + +The induction hypothesis is that all numbers less than a given number satisfy the motive, which +should be demonstrated for the given number. +-/ @[elab_as_elim] protected noncomputable def strongRecOn {motive : Nat → Sort u} (n : Nat) (ind : ∀ n, (∀ m, m < n → motive m) → motive n) : motive n := Nat.lt_wfRel.wf.fix ind n +/-- +Case analysis based on strong induction for the natural numbers. +-/ @[elab_as_elim] protected noncomputable def caseStrongRecOn {motive : Nat → Sort u} (a : Nat) diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index dfe5be7afd..c0e8a50dfb 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -20,7 +20,7 @@ {"start": {"line": 12, "character": 4}, "end": {"line": 12, "character": 12}}, "contents": {"value": - "```lean\nNat.zero : Nat\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : Nat\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 21, "character": 2}} @@ -120,7 +120,7 @@ {"start": {"line": 73, "character": 38}, "end": {"line": 73, "character": 45}}, "contents": {"value": - "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n\n***\n*import Init.Prelude*", + "```lean\nNat.add : Nat → Nat → Nat\n```\n***\nAddition of natural numbers, typically used via the `+` operator.\n\nThis function is overridden in both the kernel and the compiler to efficiently evaluate using the\narbitrary-precision arithmetic library. The definition provided here is the logical model.\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 77, "character": 10}} @@ -128,7 +128,7 @@ {"start": {"line": 77, "character": 7}, "end": {"line": 77, "character": 14}}, "contents": {"value": - "```lean\nNat\n```\n***\nAddition of natural numbers.\n\nThis definition is overridden in both the kernel and the compiler to efficiently\nevaluate using the \"bignum\" representation (see `Nat`). The definition provided\nhere is the logical model (and it is soundness-critical that they coincide).\n", + "```lean\nNat\n```\n***\nAddition of natural numbers, typically used via the `+` operator.\n\nThis function is overridden in both the kernel and the compiler to efficiently evaluate using the\narbitrary-precision arithmetic library. The definition provided here is the logical model.\n", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 82, "character": 7}} @@ -136,7 +136,7 @@ {"start": {"line": 82, "character": 7}, "end": {"line": 82, "character": 8}}, "contents": {"value": - "```lean\nNat : Type\n```\n***\nThe type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from Lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n\n***\n*import Init.Prelude*", + "```lean\nNat : Type\n```\n***\nThe natural numbers, starting at zero.\n\nThis type is special-cased by both the kernel and the compiler, and overridden with an efficient\nimplementation. Both use a fast arbitrary-precision arithmetic library (usually\n[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 87, "character": 14}} @@ -521,7 +521,7 @@ {"start": {"line": 257, "character": 4}, "end": {"line": 257, "character": 9}}, "contents": {"value": - "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 257, "character": 15}} @@ -530,7 +530,7 @@ "end": {"line": 257, "character": 18}}, "contents": {"value": - "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 260, "character": 6}} @@ -538,7 +538,7 @@ {"start": {"line": 260, "character": 4}, "end": {"line": 260, "character": 9}}, "contents": {"value": - "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 260, "character": 17}} @@ -547,7 +547,7 @@ "end": {"line": 260, "character": 20}}, "contents": {"value": - "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : ℕ) : ℕ\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 263, "character": 27}} @@ -565,7 +565,7 @@ "end": {"line": 263, "character": 36}}, "contents": {"value": - "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, is the smallest natural number. This is one of the two\nconstructors of `Nat`. Using `Nat.zero` should usually be avoided in favor of\n`0 : Nat` or simply `0`, in order to remain compatible with the simp normal\nform defined by `Nat.zero_eq`. \n***\n*import Init.Prelude*", + "```lean\nNat.zero : ℕ\n```\n***\nZero, the smallest natural number.\n\nUsing `Nat.zero` explicitly should usually be avoided in favor of the literal `0`, which is the\n[simp normal form](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hover.lean"}, "position": {"line": 269, "character": 2}} diff --git a/tests/lean/interactive/hoverDot.lean.expected.out b/tests/lean/interactive/hoverDot.lean.expected.out index 2146a7314e..d9838408d4 100644 --- a/tests/lean/interactive/hoverDot.lean.expected.out +++ b/tests/lean/interactive/hoverDot.lean.expected.out @@ -20,7 +20,7 @@ {"start": {"line": 12, "character": 14}, "end": {"line": 12, "character": 18}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 16, "character": 11}} @@ -34,7 +34,7 @@ {"start": {"line": 16, "character": 14}, "end": {"line": 16, "character": 18}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 19, "character": 13}} @@ -48,7 +48,7 @@ {"start": {"line": 19, "character": 16}, "end": {"line": 19, "character": 20}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}} {"textDocument": {"uri": "file:///hoverDot.lean"}, "position": {"line": 22, "character": 14}} @@ -62,5 +62,5 @@ {"start": {"line": 22, "character": 17}, "end": {"line": 22, "character": 21}}, "contents": {"value": - "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor function on natural numbers, `succ n = n + 1`.\nThis is one of the two constructors of `Nat`. Using `succ n` should usually\nbe avoided in favor of `n + 1`, in order to remain compatible with the simp\nnormal form defined by `Nat.succ_eq_add_one`. \n***\n*import Init.Prelude*", + "```lean\nNat.succ (n : Nat) : Nat\n```\n***\nThe successor of a natural number `n`.\n\nUsing `Nat.succ n` should usually be avoided in favor of `n + 1`, which is the [simp normal\nform](https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=simp-normal-forms).\n\n***\n*import Init.Prelude*", "kind": "markdown"}}