From 03040618b8f9b35b7b757858483e57340900cdc4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 6 May 2024 15:55:07 -0700
Subject: [PATCH] chore: test for issue #4064

closes #4064
---
 tests/lean/run/4064.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 tests/lean/run/4064.lean

diff --git a/tests/lean/run/4064.lean b/tests/lean/run/4064.lean
new file mode 100644
index 000000000000..8a2ee3b627c3
--- /dev/null
+++ b/tests/lean/run/4064.lean
@@ -0,0 +1,11 @@
+import Lean
+
+def test : Lean.CoreM (List Lean.Name) := do
+  let .thmInfo tval ← Lean.getConstInfo `And.left | unreachable!
+  return tval.all
+
+/--
+info: [`And.left]
+-/
+#guard_msgs in
+#eval test