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

feat(frontends/lean/definition_cmds): add support for 'sorry'

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-13 16:25:29 -07:00
parent 9e3bf4bd8d
commit 940382c3bc
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -119,6 +119,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_pr
buffer<name> lp_names;
buffer<expr> fns, params;
expr val = parse_mutual_definition(p, kind, lp_names, fns, params);
if (p.used_sorry()) p.declare_sorry();
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
@ -273,6 +274,7 @@ environment xdefinition_cmd_core(parser & p, def_cmd_kind kind, bool is_private,
expr fn, val;
auto header_pos = p.pos();
std::tie(fn, val) = parse_definition(p, lp_names, params);
if (p.used_sorry()) p.declare_sorry();
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);