From 594e3ea8fc14eee7a32b8d4ae00eaf9ed4434c54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Nov 2014 14:50:12 -0800 Subject: [PATCH] fix(frontends/lean/structure_cmd): 'rec' must be marked as protected --- src/frontends/lean/structure_cmd.cpp | 6 +++++- tests/lean/record_rec_protected.lean | 8 ++++++++ tests/lean/record_rec_protected.lean.expected.out | 1 + 3 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 tests/lean/record_rec_protected.lean create mode 100644 tests/lean/record_rec_protected.lean.expected.out diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 527d0e954..3f7f47ba4 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/unifier.h" #include "library/module.h" +#include "library/protected.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" @@ -524,8 +525,11 @@ struct structure_cmd_fn { inductive::inductive_decl decl(m_name, structure_type, to_list(intro)); m_env = module::add_inductive(m_env, lnames, m_params.size(), to_list(decl)); save_info(m_name, "structure", m_name_pos); - save_info(inductive::get_elim_name(m_name), "recursor", m_name_pos); + name rec_name = inductive::get_elim_name(m_name); + save_info(rec_name, "recursor", m_name_pos); save_info(m_mk, "intro", m_mk_pos); + m_env = add_namespace(m_env, m_name); + m_env = add_protected(m_env, rec_name); } void declare_projections() { diff --git a/tests/lean/record_rec_protected.lean b/tests/lean/record_rec_protected.lean new file mode 100644 index 000000000..a84cdf02b --- /dev/null +++ b/tests/lean/record_rec_protected.lean @@ -0,0 +1,8 @@ +import logic data.unit + +structure point (A : Type) (B : Type) := +mk :: (x : A) (y : B) + +open point + +check rec -- error, rec is protected diff --git a/tests/lean/record_rec_protected.lean.expected.out b/tests/lean/record_rec_protected.lean.expected.out new file mode 100644 index 000000000..891e8d3ec --- /dev/null +++ b/tests/lean/record_rec_protected.lean.expected.out @@ -0,0 +1 @@ +record_rec_protected.lean:8:6: error: unknown identifier 'rec'