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

refactor(frontends/lean/notation_cmd): remove unnecessary uses of add_local_expr

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-08 17:40:04 -07:00
parent 57c85221fe
commit 0651496bf6
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -208,7 +208,7 @@ static void parse_notation_local(parser & p, buffer<expr> & locals) {
p.next(); p.next();
expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
expr l = mk_local(n, local_type); // remark: the type doesn't matter expr l = mk_local(n, local_type); // remark: the type doesn't matter
p.add_local_expr(n, l); p.add_local(l);
locals.push_back(l); locals.push_back(l);
} else { } else {
throw parser_error("invalid notation declaration, identifier expected", p.pos()); throw parser_error("invalid notation declaration, identifier expected", p.pos());
@ -347,7 +347,7 @@ notation_entry parse_notation_core(parser & p, bool overload, buffer<token_entry
action a = parse_action(p, tk, default_prec, locals, new_tokens); action a = parse_action(p, tk, default_prec, locals, new_tokens);
expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
expr l = mk_local(n, local_type); expr l = mk_local(n, local_type);
p.add_local_expr(n, l); p.add_local(l);
locals.push_back(l); locals.push_back(l);
ts.push_back(transition(tk, a)); ts.push_back(transition(tk, a));
} else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || p.curr_is_token(get_assign_tk())) { } else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || p.curr_is_token(get_assign_tk())) {