diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 27ede6dbc7..9db9c85116 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -45,10 +45,9 @@ pushLeading >> symbol sym lbp >> termParser lbp @[builtinTermParser] def hole := parser! symbol "_" appPrec @[builtinTermParser] def «sorry» := parser! symbol "sorry" appPrec @[builtinTermParser] def cdot := parser! symbol "·" appPrec -def namedArgument := parser! " := " >> termParser def typeAscription := parser! " : " >> termParser def tupleTail := parser! ", " >> sepBy1 termParser ", " -def parenSpecial : Parser := optional (tupleTail <|> typeAscription <|> namedArgument) +def parenSpecial : Parser := optional (tupleTail <|> typeAscription) @[builtinTermParser] def paren := parser! symbol "(" appPrec >> optional (termParser >> parenSpecial) >> ")" @[builtinTermParser] def anonymousCtor := parser! symbol "⟨" appPrec >> sepBy1 termParser ", " >> "⟩" @[inline] def optIdent : Parser := optional (try (ident >> " : ")) @@ -79,7 +78,8 @@ def bracktedBinder (requireType := false) := explicitBinder requireType <|> impl def simpleBinder := parser! many1 binderIdent @[builtinTermParser] def «forall» := parser! unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracktedBinder) >> ", " >> termParser -@[builtinTermParser] def app := tparser! pushLeading >> termParser appPrec +def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")" +@[builtinTermParser] def app := tparser! pushLeading >> (namedArgument <|> termParser appPrec) @[builtinTermParser] def proj := tparser! pushLeading >> symbolNoWs "." (appPrec+1) >> (fieldIdx <|> ident) @[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25 @[builtinTermParser] def array := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]" diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean index 23a636d932..12c847300e 100644 --- a/tests/playground/termparsertest1.lean +++ b/tests/playground/termparsertest1.lean @@ -19,7 +19,7 @@ do env ← mkEmptyEnvironment; termPTables ← builtinTermParsingTable.get; match runParser env termPTables input "" "expr" with -| Except.ok _ => throw "unexpected success" +| Except.ok stx => throw (IO.userError ("unexpected success\n" ++ toString stx)) | Except.error msg => IO.println ("failed as expected, error: " ++ msg) def testFailures (is : List String) : IO Unit := @@ -77,5 +77,6 @@ test [ "∀ x y (z : Nat), x > y -> x > y - z" ]; testFailures [ -"f {x : a} -> b" +"f {x : a} -> b", +"(x := 20)" ]