From 6ae510cea46bbdb318950f78f82e9455e15a5cd0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Dec 2019 09:11:39 -0800 Subject: [PATCH] fix: reject inductive datatypes with duplicate constructor names --- src/kernel/inductive.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 2e58b97e71..539f9623d0 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -347,8 +347,13 @@ public: void check_constructors() { for (unsigned idx = 0; idx < m_ind_types.size(); idx++) { inductive_type const & ind_type = m_ind_types[idx]; + name_set found_cnstrs; for (constructor const & cnstr : ind_type.get_cnstrs()) { name const & n = constructor_name(cnstr); + if (found_cnstrs.contains(n)) { + throw kernel_exception(m_env, sstream() << "duplicate constructor name '" << n << "'"); + } + found_cnstrs.insert(n); expr t = constructor_type(cnstr); m_env.check_name(n); check_no_metavar_no_fvar(m_env, n, t);