From 77ce42548be38ff9781ad2c38b2a3a61898747e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2020 12:52:18 -0700 Subject: [PATCH] fix: add `nonReservedSymbol` --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 58346539f8..798396bef5 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -74,7 +74,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» @[builtinCommandParser] def synth := parser! "#synth " >> termParser @[builtinCommandParser] def exit := parser! "#exit" @[builtinCommandParser] def print := parser! "#print " >> (ident <|> strLit) -@[builtinCommandParser] def printAxioms := parser! "#print " >> "axioms " >> ident +@[builtinCommandParser] def printAxioms := parser! "#print " >> nonReservedSymbol "axioms " >> ident @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident @[builtinCommandParser] def «init_quot» := parser! "init_quot" @[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)