From 9f828f015ff655d8ade0408bf00d859f0c744100 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 Jul 2019 15:32:25 -0700 Subject: [PATCH] fix(library/init/lean/parser/term): allow empty anonymousCtor --- library/init/lean/parser/term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 7eb5d63549..b191c5635f 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -55,7 +55,7 @@ def typeAscription := parser! " : " >> termParser def tupleTail := parser! ", " >> sepBy1 termParser ", " def parenSpecial : Parser := optional (tupleTail <|> typeAscription) @[builtinTermParser] def paren := parser! symbol "(" appPrec >> optional (termParser >> parenSpecial) >> ")" -@[builtinTermParser] def anonymousCtor := parser! symbol "⟨" appPrec >> sepBy1 termParser ", " >> "⟩" +@[builtinTermParser] def anonymousCtor := parser! symbol "⟨" appPrec >> sepBy termParser ", " >> "⟩" def optIdent : Parser := optional (try (ident >> " : ")) @[builtinTermParser] def «if» := parser! "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser def fromTerm := parser! " from " >> termParser