chore: update stage0

stage0/src/stdlib_flags.h

@@ -22,7 +22,6 @@ options get_default_options() {
     opts = opts.update({"quotPrecheck"}, true);
 
     opts = opts.update({"pp", "rawOnError"}, true);
-    // force stage0 update for goalDotAlt/goalCaseAlt rename
 
     // Temporary, core-only flags for editing (i.e. must be part of stage0/bin/lean). Must be synced
     // with `LEAN_EXTRA_MAKE_OPTS` build flags in src/CMakeLists.txt.

stage0/stdlib/Lean/Parser/Term.c

@@ -9106,7 +9106,7 @@ static lean_object* l_Lean_Parser_Term_inferInstanceAs___closed__17;
 LEAN_EXPORT lean_object* l_Lean_Parser_Term_inferInstanceAs;
 LEAN_EXPORT lean_object* l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs__1();
 LEAN_EXPORT lean_object* l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs__1___boxed(lean_object*);
-static const lean_string_object l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs_docString__3___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 501, .m_capacity = 501, .m_length = 496, .m_data = "`inferInstanceAs α` synthesizes an instance of type `α`, transporting it from a\ndefinitionally equal type if necessary. This is useful when `α` is definitionally equal to\nsome `α'` for which instances are registered, as it prevents leaking the definition's RHS\nat lower transparencies.\n\n`inferInstanceAs` requires an expected type from context. If you just need to synthesize an\ninstance without transporting between types, use `inferInstance` instead.\n\nSee `Lean.Meta.WrapInstance` for details.\n"};
+static const lean_string_object l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs_docString__3___closed__0_value = {.m_header = {.m_rc = 0, .m_cs_sz = 0, .m_other = 0, .m_tag = 249}, .m_size = 1572, .m_capacity = 1572, .m_length = 1568, .m_data = "`inferInstanceAs α` synthesizes an instance of type `α` and then adjusts it to conform to the\nexpected type `β`, which must be inferable from context.\n\nExample:\n```\ndef D := Nat\ninstance : Inhabited D := inferInstanceAs (Inhabited Nat)\n```\n\nThe adjustment will make sure that when the resulting instance will not \"leak\" the RHS `Nat` when\nreduced at transparency levels below `semireducible`, i.e. where `D` would not be unfolded either,\npreventing \"defeq abuse\".\n\nMore specifically, given the \"source type\" (the argument) and \"target type\" (the expected type),\n`inferInstanceAs` synthesizes an instance for the source type and then unfolds and rewraps its\ncomponents (fields, nested instances) as necessary to make them compatible with the target type. The\nindividual steps are represented by the following options, which all default to enabled and can be\ndisabled to help with porting:\n\n* `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs`\n  and the default deriving handler\n* `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type\n  for sub-instance fields to avoid non-defeq instance diamonds\n* `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions\n* `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are\n  always wrapped)\n\nIf you just need to synthesize an instance without transporting between types, use `inferInstance`\ninstead, potentially with a type annotation for the expected type.\n"};
 static const lean_object* l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs_docString__3___closed__0 = (const lean_object*)&l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs_docString__3___closed__0_value;
 LEAN_EXPORT lean_object* l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs_docString__3();
 LEAN_EXPORT lean_object* l_Lean_Parser_Term_inferInstanceAs___regBuiltin_Lean_Parser_Term_inferInstanceAs_docString__3___boxed(lean_object*);