diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 28ee51e91..09daad7a5 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -267,18 +267,9 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { if (is_theorem) { if (p.num_threads() > 1) { // add as axiom, and create a task to prove the theorem - expr saved_type = type; - expr saved_value = value; - environment saved_env = env; - local_level_decls saved_lls = p.get_local_level_decls(); + p.add_delayed_theorem(env, real_n, ls, type, value); std::tie(type, new_ls) = p.elaborate_type(type); env = module::add(env, check(env, mk_axiom(real_n, append(ls, new_ls), type))); - p.add_delayed_theorem([=, &p]() { - level_param_names new_ls; - expr type, value; - std::tie(type, value, new_ls) = p.elaborate_definition_at(saved_env, saved_lls, n, saved_type, saved_value); - return check(saved_env, mk_theorem(real_n, append(ls, new_ls), type, value)); - }); } else { std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value); env = module::add(env, check(env, mk_theorem(real_n, append(ls, new_ls), type, value))); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 30da3289f..67882a72d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" +#include "kernel/type_checker.h" #include "library/parser_nested_exception.h" #include "library/aliases.h" #include "library/private.h" @@ -1077,6 +1078,16 @@ bool parser::parse_commands() { return !m_found_errors; } +void parser::add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v) { + local_level_decls saved_lls = get_local_level_decls(); + m_theorem_queue.add([=]() { + level_param_names new_ls; + expr type, value; + std::tie(type, value, new_ls) = elaborate_definition_at(env, saved_lls, n, t, v); + return check(env, mk_theorem(n, append(ls, new_ls), type, value)); + }); +} + bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads) { parser p(env, ios, in, strm_name, use_exceptions, num_threads); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 73920f231..28ba2dca9 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -162,7 +162,7 @@ public: expr mk_app(std::initializer_list const & args, pos_info const & p); unsigned num_threads() const { return m_num_threads; } - void add_delayed_theorem(std::function const & fn) { m_theorem_queue.add(fn); } + void add_delayed_theorem(environment const & env, name const & n, level_param_names const & ls, expr const & t, expr const & v); /** \brief Read the next token. */ void scan() { m_curr = m_scanner.scan(m_env); }