From 07bd2a8488eee017914ba0f6c8e76f49262cdc3d Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 7 Feb 2023 16:29:38 +0100
Subject: [PATCH] feat: add quot_precheck Lean.Parser.Term.explicit

---
 src/Lean/Elab/Quotation/Precheck.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index 31b57d84f6..c0df85c2cb 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -123,6 +123,11 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
   | `(($e :)) => precheck e
   | _ => throwUnsupportedSyntax
 
+@[builtin_quot_precheck Lean.Parser.Term.explicit] def precheckExplicit : Precheck
+  | `(@ $id) => do
+    precheck id
+  | _ => throwUnsupportedSyntax
+
 @[builtin_quot_precheck choice] def precheckChoice : Precheck := fun stx => do
   let checks ← stx.getArgs.mapM (_root_.observing ∘ precheck)
   let fails := checks.zip stx.getArgs |>.filterMap fun