From 80e00a87c6915e363aad3cfb5c7b346b9de510cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Jan 2020 20:38:08 -0800 Subject: [PATCH] feat: add `declare_syntax_cat` command parser --- src/Init/Lean/Parser/Command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Command.lean b/src/Init/Lean/Parser/Command.lean index ddbf119568..a2506a7357 100644 --- a/src/Init/Lean/Parser/Command.lean +++ b/src/Init/Lean/Parser/Command.lean @@ -94,7 +94,8 @@ def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident def openRenaming := parser! try (ident >> "renaming") >> sepBy1 openRenamingItem ", " def openOnly := parser! try (ident >> "(") >> many1 ident >> ")" def openSimple := parser! many1 ident -@[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple) +@[builtinCommandParser] def «open» := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple) +@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident /- Lean3 command declaration commands -/ def maxPrec := parser! symbolOrIdent "max"