max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add dotIdent parser

Browse source 
see #944
This commit is contained in:
Leonardo de Moura 2022-03-10 16:04:41 -08:00
parent 3214a20d33
commit 1c99fe92ac
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Term.lean
View file

@ -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 >> ")"