From 4b05c645bb7bdd01b28d4fa1faaabac80a8c31ba Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 8 Jun 2017 10:17:21 +0200 Subject: [PATCH] fix(library/constructions/injective): use same transparency setting as no_confusion --- src/library/constructions/injective.cpp | 3 ++- tests/lean/run/injection.lean | 2 ++ 2 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/injection.lean diff --git a/src/library/constructions/injective.cpp b/src/library/constructions/injective.cpp index 6246bb9e34..917af6c34b 100644 --- a/src/library/constructions/injective.cpp +++ b/src/library/constructions/injective.cpp @@ -58,7 +58,8 @@ static void collect_args(type_context & tctx, expr const & type, unsigned num_pa } expr mk_injective_type(environment const & env, name const & ir_name, expr const & ir_type, unsigned num_params, level_param_names const & lp_names) { - type_context tctx(env); + // The transparency needs to match the kernel since we need to be consistent with the no_confusion construction. + type_context tctx(env, transparency_mode::All); buffer params, args1, args2, new_args; collect_args(tctx, ir_type, num_params, params, args1, args2, new_args); expr c_ir_params = mk_app(mk_constant(ir_name, param_names_to_levels(lp_names)), params); diff --git a/tests/lean/run/injection.lean b/tests/lean/run/injection.lean new file mode 100644 index 0000000000..fca7cf494d --- /dev/null +++ b/tests/lean/run/injection.lean @@ -0,0 +1,2 @@ +inductive term +| abs : tt → term → term