From a08bc408c81f8b4f1353ebee08149e6109745d19 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Feb 2016 16:15:18 -0800 Subject: [PATCH] fix(frontends/lean/structure_cmd): fixes #967 --- src/frontends/lean/structure_cmd.cpp | 10 +++++++++- tests/lean/run/967.lean | 9 +++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/967.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index ff4bfa8ca7..df9e91f989 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/error_msgs.h" #include "kernel/inductive/inductive.h" +#include "library/trace.h" #include "library/scoped_ext.h" #include "library/normalize.h" #include "library/placeholder.h" @@ -307,8 +308,15 @@ struct structure_cmd_fn { for (expr const & p : m_params) ::lean::collect_locals(mlocal_type(p), dep_set); collect_annonymous_inst_implicit(m_p, dep_set); + /* Copy the locals from dep_set that are NOT in m_params to dep_set_minus_params */ + buffer dep_set_minus_params; + for (auto d : dep_set.get_collected()) { + if (std::all_of(m_params.begin(), m_params.end(), [&](expr const & p) { return mlocal_name(d) != mlocal_name(p); })) + dep_set_minus_params.push_back(d); + } + /* Sort dep_set_minus_params and store result in ctx */ buffer ctx; - sort_locals(dep_set.get_collected(), m_p, ctx); + sort_locals(dep_set_minus_params, m_p, ctx); expr tmp = Pi_as_is(ctx, Pi(tmp_locals, m_type, m_p), m_p); level_param_names new_ls; diff --git a/tests/lean/run/967.lean b/tests/lean/run/967.lean new file mode 100644 index 0000000000..e3a17f00e6 --- /dev/null +++ b/tests/lean/run/967.lean @@ -0,0 +1,9 @@ +variables (A : Type) + +definition f (A : Type) (a : A) := a + +inductive bla (A : Type) := +| mk : A → bla A + +structure foo (A : Type) (f : A → A) := +(a : A)