From 51aabb9b6538b72765d4e052bf0ca1a2a5d50dff Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 1 Sep 2017 14:03:12 +0200 Subject: [PATCH] feat(frontends/lean/decl_attributes): allow user attributes on inductive types --- src/frontends/lean/decl_attributes.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 332130dbe7..efeaf738d7 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -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; }