From 6fa4691eb4dde18e5e63e00ba83530a4104e106d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Oct 2015 18:29:31 -0700 Subject: [PATCH] feat(library/type_inference): improve process_assignment --- src/library/type_inference.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/library/type_inference.cpp b/src/library/type_inference.cpp index b8bd4afd6..cd1ce9afa 100644 --- a/src/library/type_inference.cpp +++ b/src/library/type_inference.cpp @@ -606,9 +606,15 @@ bool type_inference::process_assignment(expr const & ma, expr const & v) { buffer args; expr const & m = get_app_args(ma, args); buffer locals; - for (expr const & arg : args) { - if (!is_tmp_local(arg)) - break; // is not local + for (expr & arg : args) { + expr new_arg = arg; + // try to instantiate + if (is_meta(new_arg)) + new_arg = instantiate_uvars_mvars(arg); + if (!is_local(new_arg)) + break; // it is not local + arg = new_arg; + lean_assert(is_local(arg)); if (std::any_of(locals.begin(), locals.end(), [&](expr const & local) { return mlocal_name(local) == mlocal_name(arg); })) break; // duplicate local