From 8b2db1183c899b4a438ad4b0c360969a4b091e70 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 19 Jul 2024 08:57:35 -0700
Subject: [PATCH] fix: add term elaborator for `Lean.Parser.Term.namedPattern`

---
 src/Lean/Elab/BuiltinTerm.lean |  3 +++
 tests/lean/run/4662.lean       | 15 +++++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 tests/lean/run/4662.lean

diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 82e8225e5c6d..d33a54bb40c6 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -362,4 +362,7 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
     mkStrLit <$> IO.FS.readFile path
   | _, _ => throwUnsupportedSyntax
 
+@[builtin_term_elab Lean.Parser.Term.namedPattern] def elabNamedPatternErr : TermElab := fun stx _ =>
+  throwError "`<identifier>@<term>` is a named pattern and can only be used in pattern matching contexts{indentD stx}"
+
 end Lean.Elab.Term
diff --git a/tests/lean/run/4662.lean b/tests/lean/run/4662.lean
new file mode 100644
index 000000000000..2c5273b75ce6
--- /dev/null
+++ b/tests/lean/run/4662.lean
@@ -0,0 +1,15 @@
+/--
+error: `<identifier>@<term>` is a named pattern and can only be used in pattern matching contexts
+  p@()
+-/
+#guard_msgs in
+def minimal : Unit -> Unit := by
+  intro i
+  let k:p@() := i
+  sorry
+
+def minimal2 : Unit -> Unit := by
+  intro i
+  let p@k:() := i
+  guard_hyp k : p = ()
+  exact ()