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

fix: notation for non reserved symbols

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-17 11:25:04 -08:00
parent 8fa5c0ddb9
commit 8751bbe2a8
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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

2
tests/lean/nonReserved.lean
View file

@ -1,4 +1,4 @@
syntax "foo" !"bla" term : term
syntax "foo" &"bla" term : term
macro_rules
| `(foo bla $x) => x