From 0275d23ad7ca1a79b82207c5f416bac1fca39e3e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Sep 2020 17:54:12 -0700
Subject: [PATCH] fix: ignore `$` at `notFollowedByCategoryToken` when inside
 quotations

---
 src/Lean/Parser/Extension.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 9bf260b66d..1010645198 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -482,7 +482,8 @@ fun ctx s =>
     let (s, stx) := peekToken ctx s;
     match stx with
     | some (Syntax.atom _ sym) =>
-      match cat.tables.leadingTable.find? (mkNameSimple sym) with
+      if ctx.insideQuot && sym == "$" then s
+      else match cat.tables.leadingTable.find? (mkNameSimple sym) with
       | some _ => s.mkError "notFollowedByCategoryToken"
       | _      => s
     | _ => s