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

fix(library/init/lean/parser/command): variable may take unbracketed binder

Browse source
This commit is contained in:
Sebastian Ullrich 2018-10-02 09:24:31 -07:00
parent fc5120290f
commit b8b39585ec
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/lean/parser/command.lean
View file

@ -54,7 +54,7 @@ node! «namespace» ["namespace", name: ident.parser]
@[derive parser.has_tokens]
def variable.parser : command_parser :=
node! «variable» ["variable", binder: term.bracketed_binder.parser]
node! «variable» ["variable", binder: term.binder.parser]
@[derive parser.has_tokens]
def variables.parser : command_parser :=

7
library/init/lean/parser/term.lean
View file

@ -121,6 +121,13 @@ node_choice! bracketed_binder {
anonymous_constructor: anonymous_constructor.parser,
}
@[derive has_tokens has_view]
def binder.parser : term_parser :=
node_choice! binder {
bracketed: bracketed_binder.parser,
unbracketed: binder_content.parser,
}
@[derive has_tokens has_view]
def binders.parser : term_parser :=
node! binders [