chore: update stage0

stage0/stdlib/Lean/Elab/BuiltinNotation.c

@@ -16516,7 +16516,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_expandParen_docString___
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("Try to expand `·` notation.\nRecall that in Lean the `·` notation must be surrounded by parentheses.\nWe may change this is the future, but right now, here are valid examples\n- `(· + 1)`\n- `(f ⟨·, 1⟩ ·)`\n- `(· + ·)`\n- `(f · a b)` ", 240);
+x_1 = lean_mk_string_from_bytes("You can use parentheses for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- Creating simple functions when combined with `·`. Here are some examples:\n  - `(· + 1)` is shorthand for `fun x => x + 1`\n  - `(· + ·)` is shorthand for `fun x y => x + y`\n  - `(f · a b)` is shorthand for `fun x => f x a b`\n  - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n", 625);
 return x_1;
 }
 }
@@ -19865,7 +19865,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabSubst_docString___cl
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("`h ▸ e` is a macro built on top of `Eq.subst` and `Eq.symm` definitions.\nGiven `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.\nYou can also view `h ▸ e` as a \"type casting\" operation where you change the type of `e` by using `h`.\nSee the Chapter \"Quantifiers and Equality\" in the manual \"Theorem Proving in Lean\" for additional information.\n", 359);
+x_1 = lean_mk_string_from_bytes("`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions.\nGiven `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`.\nYou can also view `h ▸ e` as a \"type casting\" operation where you change the type of `e` by using `h`.\nSee the Chapter \"Quantifiers and Equality\" in the manual \"Theorem Proving in Lean\" for additional information.\n", 357);
 return x_1;
 }
 }

stage0/stdlib/Lean/Elab/Calc.c

@@ -5604,7 +5604,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabCalc_docString___clo
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("Step-wise reasoning over transitive relations.\n```\ncalc\n  a = b := pab\n  b = c := pbc\n  ...\n  y = z := pyz\n```\nproves `a = z` from the given step-wise proofs. `=` can be replaced with any\nrelation implementing the typeclass `Trans`. Instead of repeating the right-\nhand sides, subsequent left-hand sides can be replaced with `_`. ", 330);
+x_1 = lean_mk_string_from_bytes("Elaborator for the `calc` term mode variant. ", 45);
 return x_1;
 }
 }

stage0/stdlib/Lean/Elab/Match.c

@@ -46550,7 +46550,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabMatch_docString___cl
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("Pattern matching. `match e, ... with | p, ... => f | ...` matches each given\nterm `e` against each pattern `p` of a match alternative. When all patterns\nof an alternative match, the `match` term evaluates to the value of the\ncorresponding right-hand side `f` with the pattern variables bound to the\nrespective matched values. ", 326);
+x_1 = lean_mk_string_from_bytes("Pattern matching. `match e, ... with | p, ... => f | ...` matches each given\nterm `e` against each pattern `p` of a match alternative. When all patterns\nof an alternative match, the `match` term evaluates to the value of the\ncorresponding right-hand side `f` with the pattern variables bound to the\nrespective matched values.\nWhen not constructing a proof, `match` does not automatically substitute variables\nmatched on in dependent variables' types. Use `match (generalizing := true) ...` to\nenforce this. ", 507);
 return x_1;
 }
 }

stage0/stdlib/Lean/Elab/Quotation.c

@@ -43045,7 +43045,7 @@ static lean_object* _init_l___regBuiltin_Lean_Elab_Term_Quotation_elabMatchSynta
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("Syntactic pattern match. Matches a `Syntax` value against quotations, pattern variables, or `_`. ", 97);
+x_1 = lean_mk_string_from_bytes("Syntactic pattern match. Matches a `Syntax` value against quotations, pattern variables, or `_`.\n\n  Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly.\n\n  `Syntax.atom`s are ignored during matching by default except when part of a built-in literal.\n  For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching.\n  For example, in\n  ```lean\n  syntax \"c\" (\"foo\" <|> \"bar\") ...\n  ```\n  `foo` and `bar` are indistinguishable during matching, but in\n  ```lean\n  syntax foo := \"foo\"\n  syntax \"c\" (foo <|> \"bar\") ...\n  ```\n  they are not. ", 680);
 return x_1;
 }
 }

stage0/stdlib/Lean/Parser/Command.c

@@ -5508,7 +5508,7 @@ static lean_object* _init_l___regBuiltin_Lean_Parser_Term_quot_docString___close
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like\n`` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.\nMultiple command will be put in a `` `null `` node, but a single command will not (so that you can directly\nmatch against a quotation in a command kind's elaborator). ", 376);
+x_1 = lean_mk_string_from_bytes("Syntax quotation for terms. ", 28);
 return x_1;
 }
 }