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