From a5bcebb07fcfc774b6410c7687fb48030a5fb46c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Jan 2020 12:57:28 -0800
Subject: [PATCH] feat: add antiquotation support for `strLit`, `numLit` and
 `charLit`

---
 src/Init/Lean/Parser/Parser.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index 1d8618e5a9..b841a90258 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1070,7 +1070,7 @@ fun _ c s =>
   let s      := tokenFn c s;
   if s.hasError || !(s.stxStack.back.isOfKind numLitKind) then s.mkErrorAt "numeral" iniPos else s
 
-@[inline] def numLit {k : ParserKind} : Parser k :=
+@[inline] def numLitNoAntiquot {k : ParserKind} : Parser k :=
 { fn   := numLitFn,
   info := mkAtomicInfo "numLit" }
 
@@ -1080,7 +1080,7 @@ fun _ c s =>
   let s := tokenFn c s;
   if s.hasError || !(s.stxStack.back.isOfKind strLitKind) then s.mkErrorAt "string literal" iniPos else s
 
-@[inline] def strLit {k : ParserKind} : Parser k :=
+@[inline] def strLitNoAntiquot {k : ParserKind} : Parser k :=
 { fn   := strLitFn,
   info := mkAtomicInfo "strLit" }
 
@@ -1090,7 +1090,7 @@ fun _ c s =>
   let s := tokenFn c s;
   if s.hasError || !(s.stxStack.back.isOfKind charLitKind) then s.mkErrorAt "character literal" iniPos else s
 
-@[inline] def charLit {k : ParserKind} : Parser k :=
+@[inline] def charLitNoAntiquot {k : ParserKind} : Parser k :=
 { fn   := charLitFn,
   info := mkAtomicInfo "charLit" }
 
@@ -1476,6 +1476,15 @@ mkAntiquot "ident" `ident <|> identNoAntiquot
 def rawIdent {k : ParserKind} : Parser k :=
 mkAntiquot "ident" `ident <|> rawIdentNoAntiquot
 
+def numLit {k : ParserKind} : Parser k :=
+mkAntiquot "numLit" numLitKind <|> numLitNoAntiquot
+
+def strLit {k : ParserKind} : Parser k :=
+mkAntiquot "strLit" strLitKind <|> strLitNoAntiquot
+
+def charLit {k : ParserKind} : Parser k :=
+mkAntiquot "charLit" charLitKind <|> charLitNoAntiquot
+
 def categoryParserOfStackFn (offset : Nat) : ParserFn leading :=
 fun rbp ctx s =>
   let stack := s.stxStack;