From 3e05b0641bf882d5142327b1013fb8bf38e4b9ab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 19 Jun 2024 15:49:33 -0700
Subject: [PATCH] chore: fix test

---
 tests/lean/run/constructor_as_variable.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/constructor_as_variable.lean b/tests/lean/run/constructor_as_variable.lean
index eaf73cf961..78d964b44c 100644
--- a/tests/lean/run/constructor_as_variable.lean
+++ b/tests/lean/run/constructor_as_variable.lean
@@ -97,7 +97,7 @@ Suggestions:
   'Array.Mem.mk',
   'Array.mk',
   'BEq.mk',
-   (or 199 others)
+   (or 200 others)
 -/
 #guard_msgs in
 def ctorSuggestion1 (pair : α × β) : β :=