feat: elaborate arbitrary_or_ofNonempty% and use it to define constants

src/Lean/Elab/DefView.lean

@@ -132,7 +132,7 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
   let val ← match stx[3].getOptional? with
     | some val => pure val
     | none     =>
-      let val ← `(arbitrary)
+      let val ← `(arbitrary_or_ofNonempty%)
       pure $ mkNode ``Parser.Command.declValSimple #[ mkAtomFrom stx ":=", val ]
   return {
     ref := stx, kind := DefKind.opaque, modifiers := modifiers,

src/Lean/Elab/Extra.lean

@@ -313,6 +313,19 @@ 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
 

tests/lean/sanitychecks.lean.expected.out

@@ -6,7 +6,7 @@ structural recursion cannot be used
 well-founded recursion cannot be used, 'unsound' does not take any arguments
 sanitychecks.lean:4:8-5:9: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
 sanitychecks.lean:7:7-8:9: error: 'unsafe' theorems are not allowed
-sanitychecks.lean:10:0-10:24: error: failed to synthesize instance
+sanitychecks.lean:10:0-10:24: error: failed to synthesize
   Inhabited False
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'unsound3' is not a function
   False