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

fix: missing ppSpace at set_option parser

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-13 15:52:03 -08:00
parent 15232f51d3
commit 0862df9ade
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -83,7 +83,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
@[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)
@[builtinCommandParser] def «set_option» := parser! "set_option " >> ident >> ppSpace >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
@[builtinCommandParser] def «attribute» := parser! "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
@[builtinCommandParser] def «export» := parser! "export " >> ident >> "(" >> many1 ident >> ")"
def openHiding := parser! atomic (ident >> "hiding") >> many1 ident