diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2d387f2508..696101eab9 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -654,8 +654,11 @@ static environment abstract_expr_cmd(parser & p) { } static environment compile_cmd(parser & p) { + auto pos = p.pos(); name n = p.check_constant_next("invalid #compile command, constant expected"); declaration d = p.env().get(n); + if (!d.is_definition()) + throw parser_error("invalid #compile command, declaration is not a definition", pos); buffer> procs; preprocess_rec(p.env(), d, procs); return p.env();