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

fix(frontends/lean/elaborator): fixes #1669

Browse source
This commit is contained in:
Leonardo de Moura 2017-06-18 16:12:01 -07:00
parent 0996a606d1
commit c33fd8b0fd
4 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/elaborator.cpp
View file

@ -2291,7 +2291,7 @@ bool elaborator::keep_do_failure_eq(expr const & first_eq) {
return is_app(type) && is_monad_fail(app_fn(type));
}
expr elaborator::mk_aux_meta_def(expr const & e) {
expr elaborator::mk_aux_meta_def(expr const & e, expr const & ref) {
name aux_name(m_decl_name, "_aux_meta");
aux_name = aux_name.append_after(m_aux_meta_idx);
m_aux_meta_idx++;
@ -2299,7 +2299,9 @@ expr elaborator::mk_aux_meta_def(expr const & e) {
metavar_context mctx = m_ctx.mctx();
std::tie(m_env, new_c) = mk_aux_definition(m_env, mctx, local_context(),
aux_name, e, optional<bool>(true));
lean_assert(is_constant(new_c));
if (!is_constant(new_c)) {
throw elaborator_exception(ref, "failed to create auxiliary definition");
}
m_env = vm_compile(m_env, m_env.get(const_name(new_c)));
m_ctx.set_env(m_env);
m_ctx.set_mctx(mctx);
@ -2323,7 +2325,7 @@ expr elaborator::visit_equations(expr const & e) {
new_tacs = visit(equations_wf_tactics(e), some_expr(type));
new_tacs = enforce_type(*new_tacs, type, "well_founded_tactics object expected", ref);
if (!is_constant(*new_tacs)) {
new_tacs = mk_aux_meta_def(*new_tacs);
new_tacs = mk_aux_meta_def(*new_tacs, ref);
}
}

2
src/frontends/lean/elaborator.h
View file

@ -286,7 +286,7 @@ private:
expr mk_auto_param(expr const & name_lit, expr const & expected_type, expr const & ref);
optional<expr> process_optional_and_auto_params(expr type, expr const & ref, buffer<expr> & eta_args, buffer<expr> & new_args);
expr mk_aux_meta_def(expr const & e);
expr mk_aux_meta_def(expr const & e, expr const & ref);
public:
elaborator(environment const & env, options const & opts, name const & decl_name,

3
tests/lean/1669.lean Normal file
View file

@ -0,0 +1,3 @@
def f : ℕ → ℕ
| a := f a
using_well_founded ⟨{0}, well_founded_tactics.default_dec_tac⟩

5
tests/lean/1669.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
1669.lean:3:20: error: failed to synthesize type class instance for
⊢ has_emptyc (expr → list expr → tactic unit)
1669.lean:3:20: error: failed to synthesize type class instance for
⊢ has_insert ?m_1 (expr → list expr → tactic unit)
1669.lean:1:4: error: failed to create auxiliary definition