From e06d6aa6d4e18831ba51d6703e4abb42e9f814ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Feb 2017 16:11:43 -0800 Subject: [PATCH] feat(frontends/lean/elaborator): relax condition on match-convoy --- library/init/meta/injection_tactic.lean | 4 ++-- src/frontends/lean/elaborator.cpp | 3 +++ 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/library/init/meta/injection_tactic.lean b/library/init/meta/injection_tactic.lean index 03103a8cf8..2ba647ea9e 100644 --- a/library/init/meta/injection_tactic.lean +++ b/library/init/meta/injection_tactic.lean @@ -21,14 +21,14 @@ private meta def injection_intro : expr → list name → tactic unit h ← intro hname, ht ← infer_type h, -- Clear new hypothesis if it is of the form (a = a) - @try unit $ do { + try $ do { (lhs, rhs) ← match_eq ht, unify lhs rhs, clear h }, -- If new hypothesis is of the form (@heq A a B b) where -- A and B can be unified then convert it into (a = b) using -- the eq_of_heq lemma - @try unit $ do { + try $ do { (A, lhs, B, rhs) ← match_heq ht, unify A B, heq ← mk_app `eq [lhs, rhs], diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 81003830ee..81b999c016 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1944,11 +1944,14 @@ expr elaborator::visit_convoy(expr const & e, optional const & expected_ty } } new_fn_type = instantiate_mvars(new_fn_type); +#if 0 + /* The following check is too restrictive in do blocks. */ if (has_expr_metavar(new_fn_type)) { auto pp_fn = mk_pp_ctx(); throw elaborator_exception(ref, format("invalid match/convoy expression, type contains meta-variables") + pp_indent(pp_fn, new_fn_type)); } +#endif trace_elab(tout() << "match/convoy function type: " << new_fn_type << "\n";); expr new_eqns = visit_equations(update_equations_fn_type(eqns, new_fn_type)); expr fn = get_equations_result(new_eqns, 0);