max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: reject inductive datatypes with duplicate constructor names

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-14 09:11:39 -08:00
parent 38d2cffa7e
commit 6ae510cea4
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/inductive.cpp
View file

@ -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);