From b8b39585ecc523344db43e35868e2490fe29ca3b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 2 Oct 2018 09:24:31 -0700 Subject: [PATCH] fix(library/init/lean/parser/command): `variable` may take unbracketed binder --- library/init/lean/parser/command.lean | 2 +- library/init/lean/parser/term.lean | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index eb9d7e8e0f..b7856e1a42 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -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 := diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 680db0801a..0e69d83034 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -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 [