From 30e795a84dfad84103c4d2f0b9a8fcc996e95dfa Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 30 Dec 2019 15:18:38 +0100
Subject: [PATCH] feat: allow `$(x)` in match_syntax patterns

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

diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 98f7e01d22..5d06ec2d1b 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -209,6 +209,9 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
     --   let e := stx; ...
     let kind := if k == Name.anonymous then none else some k;
     let anti := quoted.getArg 1;
+    let anti := match_syntax anti with
+    | `(($e)) => e
+    | _       => anti;
     -- Splices should only appear inside a nullKind node, see next case
     if isAntiquotSplice quoted then unconditional $ fun _ => throwError quoted "unexpected antiquotation splice"
     else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn :=  fun rhs => `(let $anti := discr; $rhs) }
@@ -271,6 +274,9 @@ private partial def getAntiquotVarsAux : Syntax → TermElabM (List Syntax)
 | stx@(Syntax.node k args) => do
   if isAntiquot stx then
     let anti := args.get! 1;
+    let anti := match_syntax anti with
+    | `(($e)) => e
+    | _       => anti;
     if anti.isOfKind `Lean.Parser.Term.id then pure [anti]
     else throwError anti "syntax_match: antiquotation must be variable"
   else