From 8959b2ca87a67cb88ab0828db3672384ad7302fe Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Tue, 2 Jul 2024 13:44:46 +0200
Subject: [PATCH] chore: make constructor-as-variable test more robust (#4625)

The test tended to fail every time the number of structures in `Init`
changes, which turns out to be quite often.
---
 tests/lean/run/constructor_as_variable.lean | 20 ++++++--------------
 1 file changed, 6 insertions(+), 14 deletions(-)

diff --git a/tests/lean/run/constructor_as_variable.lean b/tests/lean/run/constructor_as_variable.lean
index a4df4e4b98..b585e75cf0 100644
--- a/tests/lean/run/constructor_as_variable.lean
+++ b/tests/lean/run/constructor_as_variable.lean
@@ -83,26 +83,18 @@ def x : A := A.x
 
 /-! Test the interaction with the invalid match pattern error messages -/
 
+inductive MyProd where
+  | construct : Nat → Nat → MyProd
+
 /--
 error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
 
-Suggestions:
-  'Add.mk',
-  'Alternative.mk',
-  'AndOp.mk',
-  'AndThen.mk',
-  'Antisymm.mk',
-  'Append.mk',
-  'Applicative.mk',
-  'Array.Mem.mk',
-  'Array.mk',
-  'BEq.mk',
-   (or 201 others)
+Suggestion: 'MyProd.construct' is similar
 -/
 #guard_msgs in
-def ctorSuggestion1 (pair : α × β) : β :=
+def ctorSuggestion1 (pair : MyProd) : Nat :=
   match pair with
-  | mk x y => y
+  | construct x y => y
 
 -- This test is a realistic situation if a user doesn't know how Lean namespaces work
 /--