From 2a4dc2cb5b4bbdc6a75a496b0f88484aabb1e26e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Oct 2018 16:15:47 -0700 Subject: [PATCH] fix(library/compiler/specialize): incorrect abstraction order --- src/library/compiler/specialize.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index beddd303bf..4e4039e045 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -709,9 +709,9 @@ class specialize_fn { expr new_fvar = m_lctx.mk_local_decl(fvar_name(fvars[i]), y.append_after(i+1), type, fvar_vals[i]).mk_ref(); new_let_decls.push_back(new_fvar); } + code = m_lctx.mk_lambda(new_fvars, code); code = m_lctx.mk_lambda(new_let_decls, code); code = m_lctx.mk_lambda(ctx.m_let_vars, code); - code = m_lctx.mk_lambda(new_fvars, code); code = m_lctx.mk_lambda(ctx.m_params, code); lean_assert(!has_fvar(code)); code = csimp(env(), code, m_cfg);