Update lean-toolchain for leanprover/lean4#14316

Author: leanprover-bot

Manual/BasicProps.lean

@@ -340,7 +340,7 @@ Propositional equality is typically denoted by the infix `=` operator.
 $_ ▸ $_
 ```
 When a term's type includes one side of an equality as a sub-term, it can be rewritten using the `▸` operator.
-If the both sides of the equality occur in the term's type, then the left side is rewritten to the right.
+If both sides of the equality occur in the term's type, then the left side is rewritten to the right.
 :::
 
 ## Uniqueness of Equality Proofs
@@ -372,8 +372,7 @@ def K {α : Sort u}
 
 example {α : Sort u} {a : α}
     {motive : {x : α} → x = x → Sort u}
-    {d : {x : α} → motive (Eq.refl x)}
-    {v : motive (Eq.refl a)} :
+    {d : {x : α} → motive (Eq.refl x)} :
     K (motive := motive) d a rfl = d := by
   rfl
 ```

Manual/BuildTools/Lake.lean

@@ -474,6 +474,8 @@ module.c
 module.c.o
 module.c.o.export
 module.c.o.noexport
+module.depHash
+module.depTrace
 module.deps
 module.dynlib
 module.exportInfo
@@ -498,6 +500,7 @@ module.olean
 module.olean.private
 module.olean.server
 module.precompileImports
+module.presetup
 module.setup
 module.transImports
 -/
@@ -520,6 +523,14 @@ The facets available for modules are:
 
   The module's dependencies (e.g., imports or shared libraries).
 
+: `depHash`
+
+  A hash of a module's build dependencies (e.g., imports, source, plugins).
+
+: `depTrace`
+
+  A Lake build trace data structure (i.e., composite hash and modification time) of a module's build dependencies (e.g., imports, source, plugins).
+
 : `olean`
 
  The module's {tech}[`.olean` file]. {TODO}[Once module system lands fully, add docs for `olean.private` and `olean.server`]

Manual/Grind/ConstraintPropagation.lean

@@ -135,7 +135,7 @@ builtin_grind_propagator propagateAndDown ↓And :=
     -- (a ∧ b) = True  ⇒  a = True
     pushEqTrue a <| mkApp3
       (mkConst ``Grind.eq_true_of_and_eq_true_left) a b h
-    -- (a ∧ b) = True  ⇒  B = True
+    -- (a ∧ b) = True  ⇒  b = True
     pushEqTrue b <| mkApp3
       (mkConst ``Grind.eq_true_of_and_eq_true_right) a b h
 ```

Manual/Grind/EMatching.lean

@@ -305,6 +305,8 @@ grindExt
 grindFunCC
 grindFwd
 grindGen
+grindHom
+grindHomPred
 grindInj
 grindIntro
 grindLR
@@ -643,6 +645,26 @@ norm
 {includeDocstring Lean.Parser.Attr.grindNorm}
 :::
 
+The {tactic}`grind` tactic can work with a source algebra that doesn't have a great deal of solving infrastructure (e.g. bitvectors) by “̲injecting”̲ it into another algebra that has more solving infrastructure (like natural numbers or integers).
+Homomorphism rules describe the injection from source to target, and how the injection commutes with other operations (like addition or multiplication in the case of bitvectors).
+Homomorphism predicates present additional facts that {tactic}`grind` can use about the injection (like that a bitvector of length $`n` corresponds to a natural number less than $`2^n`).
+
+:::syntax Lean.Parser.Attr.grindMod (title := "Homomorphism Rules")
+```grammar
+hom
+```
+{includeDocstring Lean.Parser.Attr.grindHom}
+:::
+
+:::syntax Lean.Parser.Attr.grindMod (title := "Homomorphism Predicates")
+```grammar
+hom_pred
+```
+{includeDocstring Lean.Parser.Attr.grindHomPred}
+:::
+
+{TODO}[Grind's hom infrastructure could use an example]
+
 {TODO}[Document `gen` modifier for `grind` patterns]
 
 # Inspecting Patterns

Manual/Language/InductiveTypes.lean

@@ -562,7 +562,7 @@ Their indices may differ.
 
 ::::keepEnv
 ::: example "Differing numbers of parameters"
-Even though `Both` and `OneOf` are not mutually recursive, they are declared in the same `mutual` block and must therefore have identical parameters:
+Even though `Both` and `Optional` are not mutually recursive, they are declared in the same `mutual` block and must therefore have identical parameters:
 ```lean (name := bothOptional) +error
 mutual
   inductive Both (α : Type u) (β : Type v) where
@@ -582,7 +582,7 @@ Note: All inductive types declared in the same `mutual` block must have the same
 
 ::::keepEnv
 ::: example "Differing parameter types"
-Even though `Many` and `OneOf` are not mutually recursive, they are declared in the same `mutual` block and must therefore have identical parameters.
+Even though `Many` and `Optional` are not mutually recursive, they are declared in the same `mutual` block and must therefore have identical parameters.
 They both have exactly one parameter, but `Many`'s parameter is not necessarily in the same universe as `Optional`'s:
 ```lean (name := manyOptional) +error
 mutual

Manual/Language/InductiveTypes/Nested.lean

@@ -119,19 +119,6 @@ inductive RTree'' (α : Type u) : Type u where
     BRTree branches α
 ```
 In this case, the function applies equally well to the translated version as it does to the original.
-:::
-
-:::paragraph
-A _palindrome_ is a list that is the same when reversed:
-```lean
-inductive Palindrome (α : Type) : List α → Prop where
-  | nil : Palindrome α []
-  | single : Palindrome α [x]
-  | cons (x : α) (p : Palindrome α xs) : Palindrome α (x :: xs ++ [x])
-```
-In this predicate, the list is an index whose type depends on the parameter, which is explicit for clarity.
-This means it cannot be used
-
 :::
 :::::
 

Manual/Quotients.lean

@@ -426,7 +426,7 @@ tag := "quotient-proofs"
 
 The fundamental tools for proving properties of elements of quotient types are the soundness axiom and the induction principle.
 The soundness axiom states that if two elements of the underlying type are related by the quotient's equivalence relation, then they are equal in the quotient type.
-The induction principle follows the structure of recursors for inductive types: in order to prove that a predicate holds all elements of a quotient type, it suffices to prove that it holds for an application of {name}`Quotient.mk` to each element of the underlying type.
+The induction principle follows the structure of recursors for inductive types: in order to prove that a predicate holds for all elements of a quotient type, it suffices to prove that it holds for an application of {name}`Quotient.mk` to each element of the underlying type.
 Because {name}`Quotient` is not an {tech}[inductive type], tactics such as {tactic}`cases` and {tactic}`induction` require that {name}`Quotient.ind` be specified explicitly with the {keyword}`using` modifier.
 
 {docstring Quotient.sound}

Manual/RecursiveDefs/PartialFixpoint.lean

@@ -363,7 +363,7 @@ tag := "mutual-partial-fixpoint"
 
 Lean supports the definition of {tech}[mutually recursive] functions using {tech}[partial fixpoint].
 Mutual recursion may be introduced using a {tech}[mutual block], but it also results from {keywordOf Lean.Parser.Term.letrec}`let rec` expressions and {keywordOf Lean.Parser.Command.declaration}`where` blocks.
-The rules for mutual well-founded recursion are applied to a group of actually mutually recursive, lifted definitions, that results from the {ref "mutual-syntax"}[elaboration steps] for mutual groups.
+The rules for mutual recursion with partial fixpoints are applied to a group of actually mutually recursive, lifted definitions, that results from the {ref "mutual-syntax"}[elaboration steps] for mutual groups.
 
 If all functions in the mutual group have the {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint` clause, then this strategy is used.
 

Manual/Releases.lean

@@ -6,6 +6,9 @@ Author: Joachim Breitner
 
 import VersoManual
 
+import Manual.Releases.«v4_33_0»
+import Manual.Releases.«v4_32_2»
+import Manual.Releases.«v4_32_1»
 import Manual.Releases.«v4_32_0»
 import Manual.Releases.«v4_31_0»
 import Manual.Releases.«v4_30_0»
@@ -63,6 +66,12 @@ This section provides release notes about recent versions of Lean. When updating
 read the corresponding release notes. They may contain advice that will help you understand
 the differences with the previous version and upgrade your projects.
 
+{include 0 Manual.Releases.«v4_33_0»}
+
+{include 0 Manual.Releases.«v4_32_2»}
+
+{include 0 Manual.Releases.«v4_32_1»}
+
 {include 0 Manual.Releases.«v4_32_0»}
 
 {include 0 Manual.Releases.«v4_31_0»}