From a438a2ee21158dfbd4750ab3abd504ccfec7b7e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Jan 2022 17:22:39 -0800
Subject: [PATCH] feat: elaborate `arbitrary_or_ofNonempty%` and use it to
 define constants

---
 src/Lean/Elab/DefView.lean                |  2 +-
 src/Lean/Elab/Extra.lean                  | 13 +++++++++++++
 tests/lean/sanitychecks.lean.expected.out |  2 +-
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 09b804cc16..731c4573a3 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/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,
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 9e510733b9..cfad6e47a0 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/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
 
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index ba21be64c6..1a5633dd6a 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/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