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

feat(frontends/lean/decl_attributes): allow user attributes on inductive types

Browse source
This commit is contained in:
Sebastian Ullrich 2017-09-01 14:03:12 +02:00
parent ea6a4159a9
commit 51aabb9b65
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/decl_attributes.cpp
View file

@ -134,8 +134,10 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
bool decl_attributes::ok_for_inductive_type() const {
for (entry const & e : m_entries) {
name const & n = e.m_attr->get_name();
if ((n != "class" && !is_class_symbol_tracking_attribute(n)) || e.deleted())
return false;
if (is_system_attribute(n)) {
if ((n != "class" && !is_class_symbol_tracking_attribute(n)) || e.deleted())
return false;
}
}
return true;
}