chore: test for issue #4064

closes #4064
leanprover · May 7, 2024 · 0304061 · 0304061
1 parent dfde4ee
commit 0304061
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/tests/lean/run/4064.lean 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