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

feat: openDecl antiquotation

Browse source
This commit is contained in:
Sebastian Ullrich 2022-08-07 15:11:07 +02:00
parent ee70805c35
commit d7e14ba47f
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -143,7 +143,8 @@ def openRenaming := leading_parser atomic (ident >> "renaming") >> sepBy1 op
def openOnly := leading_parser atomic (ident >> " (") >> many1 ident >> ")"
def openSimple := leading_parser many1 (checkColGt >> ident)
def openScoped := leading_parser "scoped " >> many1 (checkColGt >> ident)
def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
def openDecl := withAntiquot (mkAntiquot "openDecl" `Lean.Parser.Command.openDecl (isPseudoKind := true)) <|
openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped
@[builtinCommandParser] def «open» := leading_parser withPosition ("open " >> openDecl)
@[builtinCommandParser] def «mutual» := leading_parser "mutual " >> many1 (ppLine >> notSymbol "end" >> commandParser) >> ppDedent (ppLine >> "end") >> terminationSuffix