chore: bump toolchain to 4.17.0-rc1 and prepare for release (#277)

Manual.lean

@@ -52,6 +52,13 @@ Additionally, we will be adding missing API reference documentation and revising
 
 **Release History**
 
+: 2025-02-03
+
+  This release updates the contents for Lean version 4.17.0-rc1.
+  It adds descriptions of {ref "well-founded-recursion"}[well-founded recursion], the new {ref "partial-fixpoint"}[partial fixpoint] feature, {ref "quotients"}[quotient types], and {ref "lake"}[Lake], and {ref "structural-recursion"}[the description of structural recursion] has been greatly improved.
+  Descriptions and API references for all fixed-width integer types, {name}`Int`, {name}`Fin`, {name}`Empty`, {name}`Option` were also added
+  This release also includes a quick-jump box that can be used to quickly navigate to any documented topic.
+
 : 2024-12-16
 
   This is the initial release of the reference manual.

Manual/Simp.lean

@@ -427,14 +427,14 @@ example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by
 ```
 The suggested rewrite is:
 ```leanOutput simpHuhDemo
-Try this: simp only [Array.size_toArray, List.length_cons, List.length_singleton, Nat.reduceAdd]
+Try this: simp only [Array.size_toArray, List.length_cons, List.length_nil, Nat.zero_add, Nat.reduceAdd]
 ```
 which results in the more maintainable proof:
 ```lean
 example (xs : Array Unit) : xs.size = 2 → xs = #[(), ()] := by
   intros
   ext
-  simp only [Array.size_toArray, List.length_cons, List.length_singleton, Nat.reduceAdd]
+  simp only [Array.size_toArray, List.length_cons, List.length_nil, Nat.zero_add, Nat.reduceAdd]
   assumption
 ```
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c8e26eba4e1dc849e62570e6c964040db8bf3a16",
+   "rev": "b79b06e8a36f249c0bb8f778518c231b204cbde8",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1,2 +1 @@
-leanprover/lean4:nightly-2025-01-28
-
+leanprover/lean4:v4.17.0-rc1