From c31c026f4694d9f0b557d68e97908880a07df4a7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2014 17:08:31 -0700 Subject: [PATCH] feat(frontends/lean/class): accept only inductive datatypes (and records) as classes --- src/frontends/lean/class.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 306cd50e2..d10bfdcd8 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -119,8 +119,8 @@ typedef scoped_ext class_ext; static void check_class(environment const & env, name const & c_name) { declaration c_d = env.get(c_name); - if (c_d.is_definition() && !c_d.is_opaque()) - throw exception(sstream() << "invalid class, '" << c_name << "' is a transparent definition"); + if (c_d.is_definition()) + throw exception(sstream() << "invalid class, '" << c_name << "' is a definition"); } name get_class_name(environment const & env, expr const & e) { @@ -149,6 +149,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type))); } name c = get_class_name(env, get_app_fn(type)); + check_class(env, c); return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n, priority), persistent); }