michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/builtin_cmds): change mask notation at #app_builder command

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-01 19:27:25 -08:00
parent f21102a725
commit d1fa547335
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -1154,7 +1154,7 @@ static environment app_builder_cmd(parser & p) {
name c = p.check_constant_next("invalid #app_builder command, constant expected"); name c = p.check_constant_next("invalid #app_builder command, constant expected");
bool has_mask = false; bool has_mask = false;
buffer<bool> mask; buffer<bool> mask;
if (p.curr_is_token(get_lparen_tk())) { if (p.curr_is_token(get_lbracket_tk())) {
p.next(); p.next();
has_mask = true; has_mask = true;
while (true) { while (true) {
@ -1164,7 +1164,7 @@ static environment app_builder_cmd(parser & p) {
break; break;
p.next(); p.next();
} }
p.check_token_next(get_rparen_tk(), "invalid #app_builder command, ')' expected"); p.check_token_next(get_rbracket_tk(), "invalid #app_builder command, ']' expected");
} }
buffer<expr> args; buffer<expr> args;

4
tests/lean/run/app_builder3.lean
View file

@ -3,5 +3,5 @@ constant f : ∀ (A : Type) (a b c : A), a = c → A
variables a b c : nat variables a b c : nat
variables H : a = b variables H : a = b
#app_builder f (false, false, true, false, true) c, H #app_builder f [false, false, true, false, true] c, H
#app_builder f (false, true, true, false, true) a, c, H #app_builder f [false, true, true, false, true] a, c, H