From cc1c9f3dfbfcd41c1bdbb5f9beecb7e2f2a22265 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Aug 2020 12:26:07 -0700 Subject: [PATCH] feat: add `#print axioms` --- src/Lean/Parser/Command.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 8b2db5dd95..2b9c188651 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -81,7 +81,8 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> « @[builtinCommandParser] def eval := parser! "#eval " >> termParser @[builtinCommandParser] def synth := parser! "#synth " >> termParser @[builtinCommandParser] def exit := parser! "#exit" -@[builtinCommandParser] def print := parser! "#print" >> (ident <|> strLit) +@[builtinCommandParser] def print := parser! "#print " >> (ident <|> strLit) +@[builtinCommandParser] def printAxioms := parser! "#print " >> "axioms " >> optional 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)