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

fix(frontends/lean/definition_cmds): empty set of equations

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-22 13:30:37 -07:00
parent 9ad64e9176
commit f4fd0ca775
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/definition_cmds.cpp
View file

@ -144,7 +144,7 @@ expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & p
if (p.curr_is_token(get_assign_tk())) {
p.next();
val = p.parse_expr();
} else if (p.curr_is_token(get_bar_tk())) {
} else if (p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_none_tk())) {
p.add_local(fn);
buffer<expr> eqns;
if (p.curr_is_token(get_none_tk())) {