From 940382c3bcb3f2292ed3c87bfaf1749e5d7dfabc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 13 Aug 2016 16:25:29 -0700 Subject: [PATCH] feat(frontends/lean/definition_cmds): add support for 'sorry' --- src/frontends/lean/definition_cmds.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index ce3e7686dc..061c9d73f9 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -119,6 +119,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, bool is_pr buffer lp_names; buffer 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 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 new_params; elaborate_params(elab, params, new_params);