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

chore(frontents/lean/definition_cmds): improve error message

Browse source
This commit is contained in:
Daniel Selsam 2016-10-07 13:30:52 -07:00 • committed by Leonardo de Moura
parent 1644e52c47
commit 7cdec2c8f3
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -122,6 +122,9 @@ expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<expr> &
while (p.curr_is_token(get_bar_tk())) {
eqns.push_back(parse_equation(p, pre_fn));
}
if (!p.curr_is_command() && !p.curr_is_eof()) {
throw parser_error("invalid equations, must be followed by a command or EOF", p.pos());
}
}
expr fn = mk_local(mlocal_name(pre_fn), local_pp_name(pre_fn), fn_type, mk_rec_info(true));
fns.push_back(fn);
@ -177,6 +180,9 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
while (p.curr_is_token(get_bar_tk())) {
eqns.push_back(parse_equation(p, fn));
}
if (!p.curr_is_command() && !p.curr_is_eof()) {
throw parser_error("invalid equations, must be followed by a command or EOF", p.pos());
}
}
optional<expr_pair> R_Rwf = parse_using_well_founded(p);
val = mk_equations(p, fn, scope2.get_name(), eqns, R_Rwf, header_pos);