chore: update stage0

stage0/src/Lean/Elab/Extra.lean

@@ -313,6 +313,21 @@ def elabBinCalc : TermElab :=  fun stx expectedType? => do
     pure ()
   ensureHasType expectedType? result
 
+/-
+@[builtinTermElab arbitraryOrOfNonempty]
+def elabArbitraryOrNonempty : TermElab :=  fun stx expectedType? => do
+  tryPostponeIfNoneOrMVar expectedType?
+  match expectedType? with
+  | none => throwError "invalid 'arbitrary_or_ofNonempty%', expected type is not known"
+  | some expectedType =>
+    try
+      mkArbitrary expectedType
+    catch ex => try
+      mkOfNonempty expectedType
+    catch _ =>
+      throw ex
+-/
+
 builtin_initialize
   registerTraceClass `Elab.binop
 

stage0/src/Lean/Parser/Term.lean

@@ -242,6 +242,8 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
 @[builtinTermParser] def waitIfTypeContainsMVar := leading_parser "wait_if_type_contains_mvar% " >> "?" >> ident >> "; " >> termParser
 @[builtinTermParser] def waitIfContainsMVar     := leading_parser "wait_if_contains_mvar% " >> "?" >> ident >> "; " >> termParser
 
+@[builtinTermParser] def arbitraryOrOfNonempty := leading_parser "arbitrary_or_ofNonempty%"
+
 def namedArgument  := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
 def ellipsis       := leading_parser ".."
 def argument       :=