diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 8dcf6336a0..c2e3323936 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -30,7 +30,7 @@ namespace Syntax @[builtinSyntaxParser] def unary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")" @[builtinSyntaxParser] def binary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")" @[builtinSyntaxParser] def atom := parser! strLit -@[builtinSyntaxParser] def nonReserved := parser! "!" >> strLit +@[builtinSyntaxParser] def nonReserved := parser! "&" >> strLit end Syntax diff --git a/tests/lean/nonReserved.lean b/tests/lean/nonReserved.lean index 7f2ddae9b2..35de65221f 100644 --- a/tests/lean/nonReserved.lean +++ b/tests/lean/nonReserved.lean @@ -1,4 +1,4 @@ -syntax "foo" !"bla" term : term +syntax "foo" &"bla" term : term macro_rules | `(foo bla $x) => x