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