fix: add term elaborator for Lean.Parser.Term.namedPattern (#4792)

closes #4662

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

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 ()