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

chore: add back support for Lean3 mixfix/reserve syntax

Browse source 
We have tests that rely on them :(
This commit is contained in:
Leonardo de Moura 2020-09-07 16:40:12 -07:00
parent 722608d0c6
commit cf944e32cf
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Parser/Syntax.lean
View file

@ -50,7 +50,13 @@ def «infixl» := parser! "infixl"
def «infixr» := parser! "infixr"
def «postfix» := parser! "postfix"
def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «postfix»
@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> «precedence» >> strLit >> darrow >> termParser
-- TODO: after we remove old frontend
-- * remove " := "
-- * remove quotedSymbol and unquotedSymbol alternative
@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> optPrecedence >> (strLit <|> quotedSymbol <|> unquotedSymbol) >> (darrow <|> " := ") >> termParser
-- TODO: remove
@[builtinCommandParser] def «reserve» := parser! "reserve " >> mixfixKind >> quotedSymbol >> optPrecedence
def identPrec := parser! ident >> optPrecedence
def optKind : Parser := optional ("[" >> ident >> "]")