From 1c99fe92ac07dd33d4f35c90d004ee8bea796a5b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 10 Mar 2022 16:04:41 -0800
Subject: [PATCH] feat: add `dotIdent` parser

see #944
---
 src/Lean/Parser/Term.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 011642e0ab..e890ffac17 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -297,6 +297,8 @@ def macroLastArg   := macroDollarArg <|> macroArg
 
 @[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
 
+@[builtinTermParser] def dotIdent := leading_parser "." >> checkNoWsBefore >> ident
+
 end Term
 
 @[builtinTermParser default+1] def Tactic.quot    : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")"