From 804ebcec163ca61e1e0cbb6eeca3d6768bfbdd19 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 7 Sep 2020 15:48:53 -0700 Subject: [PATCH] feat: adjust `mixfix` syntax --- src/Lean/Parser/Syntax.lean | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 88cc0aa2fd..6d943cf7aa 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -49,15 +49,10 @@ def «infix» := parser! "infix" def «infixl» := parser! "infixl" def «infixr» := parser! "infixr" def «postfix» := parser! "postfix" - def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix» --- TODO delete reserve after old frontend is gone -@[builtinCommandParser] def «reserve» := parser! "reserve " >> mixfixKind >> quotedSymbol >> optPrecedence -def mixfixSymbol := (quotedSymbol >> optPrecedence /- TODO: remove precedence after we delete old precedence -/) <|> unquotedSymbol -def identPrec := parser! ident >> optPrecedence --- TODO: remove " := " after old frontend is gone -@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> optPrecedence >> mixfixSymbol >> (" := " <|> darrow) >> termParser +@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> «precedence» >> strLit >> darrow >> termParser +def identPrec := parser! ident >> optPrecedence def optKind : Parser := optional ("[" >> ident >> "]") def notationItem := withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> quotedSymbol <|> identPrec) -- TODO: remove " := " after old frontend is gone