From 9cd88807dd6158ffdb1666f05250ea27cde42676 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 11 Sep 2020 15:16:54 -0700
Subject: [PATCH] feat: add support for quoted literals in patterns

---
 src/Lean/Elab/Match.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 998e64f317..f4f878890c 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -370,6 +370,16 @@ match f? with
     | none => throwCtorExpected
   | _ => processVar stx
 
+private def nameToPattern : Name → TermElabM Syntax
+| Name.anonymous => `(Name.anonymous)
+| Name.str p s _ => do p ← nameToPattern p; `(Name.str $p $(quote s) _)
+| Name.num p n _ => do p ← nameToPattern p; `(Name.num $p $(quote n) _)
+
+private def quotedNameToPattern (stx : Syntax) : TermElabM Syntax :=
+match (stx.getArg 0).isNameLit? with
+| some val => nameToPattern val
+| none     => throwIllFormedSyntax
+
 private partial def collect : Syntax → M Syntax
 | stx@(Syntax.node k args) => withRef stx $ withFreshMacroScope $
   if k == `Lean.Parser.Term.app then do
@@ -434,6 +444,11 @@ private partial def collect : Syntax → M Syntax
     pure stx
   else if k == charLitKind then
     pure stx
+  else if k == `Lean.Parser.Term.quotedName then
+    /- Quoted names have an elaboration function associated with them, and they will not be macro expanded.
+       Note that macro expansion is not a good option since it produces a term using the smart constructors `mkNameStr`, `mkNameNum`
+       instead of the constructors `Name.str` and `Name.num` -/
+    liftM $ quotedNameToPattern stx
   else if k == choiceKind then
     throwError "invalid pattern, notation is ambiguous"
   else