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

chore: support old notation syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2020-01-19 18:45:08 +01:00
parent 7f4e1db86b
commit 15bed7c95c
2 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1100,6 +1100,7 @@ fun _ c s =>
def quotedSymbolFn {k : ParserKind} : ParserFn k :=
nodeFn `quotedSymbol (andthenFn (andthenFn (chFn '`') (rawFn (fun _ => takeUntilFn (fun c => c == '`')))) (chFn '`' true))
-- TODO: remove after old frontend is gone
def quotedSymbol {k : ParserKind} : Parser k :=
{ fn := quotedSymbolFn }

6
src/Init/Lean/Parser/Syntax.lean
View file

@ -54,11 +54,13 @@ def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «p
-- TODO delete reserve
@[builtinCommandParser] def «reserve» := parser! "reserve " >> mixfixKind >> quotedSymbolPrec
def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol
@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> mixfixSymbol >> darrow >> termParser
-- TODO: remove " := " after old frontend is gone
@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> mixfixSymbol >> (" := " <|> darrow) >> termParser
def strLitPrec := parser! strLit >> optPrecedence
def identPrec := parser! ident >> optPrecedence
@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> darrow >> termParser
-- TODO: remove " := " after old frontend is gone
@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented"
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident