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

chore: remove #resolve_name

Browse source
This commit is contained in:
Mario Carneiro 2022-10-17 16:05:42 -04:00 • committed by Leonardo de Moura
parent 8fc6a2a856
commit faa612e7b7
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -130,7 +130,6 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «opaque» <|
@[builtinCommandParser] def exit := leading_parser "#exit"
@[builtinCommandParser] def print := leading_parser "#print " >> (ident <|> strLit)
@[builtinCommandParser] def printAxioms := leading_parser "#print " >> nonReservedSymbol "axioms " >> ident
@[builtinCommandParser] def «resolve_name» := leading_parser "#resolve_name " >> ident
@[builtinCommandParser] def «init_quot» := leading_parser "init_quot"
def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
@[builtinCommandParser] def «set_option» := leading_parser "set_option " >> ident >> ppSpace >> optionValue